MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2d Unicode version

Theorem simp2d 968
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp2d  |-  ( ph  ->  ch )

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp2 956 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
31, 2syl 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp2bi  971  oeeui  6600  erinxp  6733  resixp  6851  domssex  7022  cantnflem1a  7387  cantnflem1d  7390  cantnflem3  7393  cantnflem4  7394  fpwwe2lem7  8258  canthnumlem  8270  canthp1lem2  8275  wun0  8340  supmullem2  9721  supmul  9722  ixxdisj  10671  ixxun  10672  ixxss1  10674  ixxss2  10675  ixxss12  10676  ixxub  10677  ixxlb  10678  ubioo  10688  iccss2  10720  icodisj  10761  xov1plusxeqvd  10780  fldiv  10964  immul  11621  sqrge0  11743  sqrrege0  11849  icco1  12014  ruclem2  12510  ruclem3  12511  ruclem8  12515  ruclem12  12519  gcddvds  12694  crt  12846  phimullem  12847  eulerthlem1  12849  eulerthlem2  12850  prmreclem3  12965  sectcan  13658  sectco  13659  sectmon  13680  monsect  13681  funcixp  13741  funcsect  13746  invfuc  13848  coapm  13903  catciso  13939  posasymb  14086  ipodrsima  14268  pstr2  14314  psdmrn  14316  psref  14317  mhmlin  14422  subm0cl  14429  eqger  14667  eqgcpbl  14671  gaorber  14762  orbstafun  14765  cayleyth  14790  dfod2  14877  sylow2blem1  14931  dprdf  15241  dprdff  15247  dprdfcl  15248  dprdsplit  15283  dpjcntz  15287  ablfac1a  15304  ablfac1b  15305  lmodvsdi  15650  lbssp  15832  2idlcpbl  15986  assarng  16061  pnfnei  16950  cnptop2  16973  lmcl  17025  lmcnp  17032  flimfil  17664  tlmlmod  17871  imasdsf1olem  17937  xmeter  17979  tmsds  18030  nlmlmod  18189  qdensere  18279  blcvx  18304  tgqioo  18306  icccmplem2  18328  reconnlem1  18331  cnmpt2pc  18426  phtpcer  18493  phtpcco2  18497  pcohtpylem  18517  pcohtpy  18518  pcophtb  18527  om1addcl  18531  pi1blem  18537  pi1cpbl  18542  pi1grplem  18547  pi1inv  18550  pi1xfrf  18551  pi1xfr  18553  pi1xfrcnvlem  18554  pi1cof  18557  pi1coghm  18559  cphnlm  18608  cphsqrcl2  18622  tchcph  18667  lmcau  18738  bcthlem4  18749  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  ivthicc  18818  ovolfsval  18830  ovollb2lem  18847  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem2  18877  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicopnf  18883  ioombl1lem1  18915  ioombl1lem3  18917  ioombl1lem4  18918  uniioovol  18934  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyadmaxlem  18952  volivth  18962  vitalilem2  18964  vitalilem5  18967  i1frn  19032  itg2monolem1  19105  itgcnlem  19144  itgrevallem1  19149  itgreval  19151  itgle  19164  ibladd  19175  iblabslem  19182  itgspliticc  19191  itgsplitioo  19192  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  limcdif  19226  limcresi  19235  limccnp  19241  limccnp2  19242  limcco  19243  dvlip  19340  dvlip2  19342  dveq0  19347  dvgt0lem1  19349  dvivthlem1  19355  dvcnvrelem1  19364  dvcnvre  19366  dvfsumlem2  19374  ftc1lem1  19382  ftc1a  19384  ftc1lem4  19386  ftc2ditglem  19392  itgsubstlem  19395  mpff  19425  mpfaddcl  19426  mpfmulcl  19427  mpfind  19428  pf1rcl  19432  mpfpf1  19434  ply1rem  19549  fta1glem1  19551  ig1pdvds  19562  plyrem  19685  facth  19686  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  aaliou3lem3  19724  aaliou3lem4  19726  aaliou3lem7  19729  taylfvallem1  19736  tayl0  19741  taylply2  19747  radcnvle  19796  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  abelth2  19818  coseq00topi  19870  coseq0negpitopi  19871  cosordlem  19893  tanord1  19899  efif1olem1  19904  loglesqr  20098  logreclem  20116  chordthmlem4  20132  quart1  20152  quartlem2  20154  quartlem3  20155  quartlem4  20156  quart  20157  acosbnd  20196  atancj  20206  atanlogsublem  20211  atantan  20219  atanbndlem  20221  dvatan  20231  atantayl  20233  rlimcnp2  20261  divsqrsumlem  20274  ftalem5  20314  ftalem7  20316  basellem4  20321  basellem5  20322  perfectlem2  20469  dchrinv  20500  chpdifbndlem1  20702  pntibndlem2  20740  pntlemc  20744  pntlema  20745  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemq  20750  pntlemr  20751  pntlemj  20752  pntlemi  20753  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntleme  20757  pntlem3  20758  pntleml  20760  abvcxp  20764  grpoass  20870  vcsm  21105  nvf  21224  ssps  21306  minvecolem2  21454  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  eigvec1  22542  iccgelb  23266  eliccelico  23270  elicoelioo  23271  cnre2csqlem  23294  xrge0iifhom  23319  lmxrge0  23375  logbcl  23399  rnlogbval  23402  nnlogbexp  23406  sigaclci  23493  difelsiga  23494  insiga  23498  measvnul  23536  subfacp1lem2a  23711  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  sconpht2  23769  sconpi1  23770  rescon  23777  cvmsss  23798  cvmsn0  23799  cvmlift2lem3  23836  cvmlift2lem7  23840  cvmliftphtlem  23848  cvmliftpht  23849  cvmlift3lem5  23854  cvmlift3lem6  23855  eupaf1o  23885  ghomgrplem  23996  ghomfo  23998  ghomgsg  24000  preotr1  25234  fldax3  25430  fldax4  25431  fldax5  25432  vecax2  25454  icccon3  25701  coda  25729  dualalg  25782  dualded  25783  dehm  25792  iddvvidd  25838  idcvvidc  25839  ivthALT  26258  heiborlem3  26537  iccbnd  26564  rngohom1  26599  idl0cl  26643  maxidlnr  26667  pmtrfinv  27402  stoweidlem11  27760  stoweidlem31  27780  stoweidlem36  27785  stoweidlem38  27787  stoweidlem44  27793  stoweidlem62  27811  sigardiv  27851  sigarcol  27854  sharhght  27855  sigaradd  27856  cevathlem1  27857  cevathlem2  27858  cevath  27859  lshpne  29172  opococ  29385  opexmid  29397  hlclat  29548  lclkrslem2  31728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator