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  6616  erinxp  6749  resixp  6867  domssex  7038  cantnflem1a  7403  cantnflem1d  7406  cantnflem3  7409  cantnflem4  7410  fpwwe2lem7  8274  canthnumlem  8286  canthp1lem2  8291  wun0  8356  supmullem2  9737  supmul  9738  ixxdisj  10687  ixxun  10688  ixxss1  10690  ixxss2  10691  ixxss12  10692  ixxub  10693  ixxlb  10694  ubioo  10704  iccss2  10736  icodisj  10777  xov1plusxeqvd  10796  fldiv  10980  immul  11637  sqrge0  11759  sqrrege0  11865  icco1  12030  ruclem2  12526  ruclem3  12527  ruclem8  12531  ruclem12  12535  gcddvds  12710  crt  12862  phimullem  12863  eulerthlem1  12865  eulerthlem2  12866  prmreclem3  12981  sectcan  13674  sectco  13675  sectmon  13696  monsect  13697  funcixp  13757  funcsect  13762  invfuc  13864  coapm  13919  catciso  13955  posasymb  14102  ipodrsima  14284  pstr2  14330  psdmrn  14332  psref  14333  mhmlin  14438  subm0cl  14445  eqger  14683  eqgcpbl  14687  gaorber  14778  orbstafun  14781  cayleyth  14806  dfod2  14893  sylow2blem1  14947  dprdf  15257  dprdff  15263  dprdfcl  15264  dprdsplit  15299  dpjcntz  15303  ablfac1a  15320  ablfac1b  15321  lmodvsdi  15666  lbssp  15848  2idlcpbl  16002  assarng  16077  pnfnei  16966  cnptop2  16989  lmcl  17041  lmcnp  17048  flimfil  17680  tlmlmod  17887  imasdsf1olem  17953  xmeter  17995  tmsds  18046  nlmlmod  18205  qdensere  18295  blcvx  18320  tgqioo  18322  icccmplem2  18344  reconnlem1  18347  cnmpt2pc  18442  phtpcer  18509  phtpcco2  18513  pcohtpylem  18533  pcohtpy  18534  pcophtb  18543  om1addcl  18547  pi1blem  18553  pi1cpbl  18558  pi1grplem  18563  pi1inv  18566  pi1xfrf  18567  pi1xfr  18569  pi1xfrcnvlem  18570  pi1cof  18573  pi1coghm  18575  cphnlm  18624  cphsqrcl2  18638  tchcph  18683  lmcau  18754  bcthlem4  18765  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  ivthicc  18834  ovolfsval  18846  ovollb2lem  18863  ovolshftlem1  18884  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem2  18893  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicopnf  18899  ioombl1lem1  18931  ioombl1lem3  18933  ioombl1lem4  18934  uniioovol  18950  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  dyadmaxlem  18968  volivth  18978  vitalilem2  18980  vitalilem5  18983  i1frn  19048  itg2monolem1  19121  itgcnlem  19160  itgrevallem1  19165  itgreval  19167  itgle  19180  ibladd  19191  iblabslem  19198  itgspliticc  19207  itgsplitioo  19208  ditgcl  19224  ditgswap  19225  ditgsplitlem  19226  limcdif  19242  limcresi  19251  limccnp  19257  limccnp2  19258  limcco  19259  dvlip  19356  dvlip2  19358  dveq0  19363  dvgt0lem1  19365  dvivthlem1  19371  dvcnvrelem1  19380  dvcnvre  19382  dvfsumlem2  19390  ftc1lem1  19398  ftc1a  19400  ftc1lem4  19402  ftc2ditglem  19408  itgsubstlem  19411  mpff  19441  mpfaddcl  19442  mpfmulcl  19443  mpfind  19444  pf1rcl  19448  mpfpf1  19450  ply1rem  19565  fta1glem1  19567  ig1pdvds  19578  plyrem  19701  facth  19702  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  aaliou3lem3  19740  aaliou3lem4  19742  aaliou3lem7  19745  taylfvallem1  19752  tayl0  19757  taylply2  19763  radcnvle  19812  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  abelth2  19834  coseq00topi  19886  coseq0negpitopi  19887  cosordlem  19909  tanord1  19915  efif1olem1  19920  loglesqr  20114  logreclem  20132  chordthmlem4  20148  quart1  20168  quartlem2  20170  quartlem3  20171  quartlem4  20172  quart  20173  acosbnd  20212  atancj  20222  atanlogsublem  20227  atantan  20235  atanbndlem  20237  dvatan  20247  atantayl  20249  rlimcnp2  20277  divsqrsumlem  20290  ftalem5  20330  ftalem7  20332  basellem4  20337  basellem5  20338  perfectlem2  20485  dchrinv  20516  chpdifbndlem1  20718  pntibndlem2  20756  pntlemc  20760  pntlema  20761  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemq  20766  pntlemr  20767  pntlemj  20768  pntlemi  20769  pntlemf  20770  pntlemk  20771  pntlemo  20772  pntleme  20773  pntlem3  20774  pntleml  20776  abvcxp  20780  grpoass  20886  vcsm  21121  nvf  21240  ssps  21322  minvecolem2  21470  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  eigvec1  22558  iccgelb  23281  eliccelico  23285  elicoelioo  23286  cnre2csqlem  23309  xrge0iifhom  23334  lmxrge0  23390  logbcl  23414  rnlogbval  23417  nnlogbexp  23421  sigaclci  23508  difelsiga  23509  insiga  23513  measvnul  23551  subfacp1lem2a  23726  subfacp1lem3  23728  subfacp1lem4  23729  subfacp1lem5  23730  sconpht2  23784  sconpi1  23785  rescon  23792  cvmsss  23813  cvmsn0  23814  cvmlift2lem3  23851  cvmlift2lem7  23855  cvmliftphtlem  23863  cvmliftpht  23864  cvmlift3lem5  23869  cvmlift3lem6  23870  eupaf1o  23900  ghomgrplem  24011  ghomfo  24013  ghomgsg  24015  ibladdnc  25008  iblabsnclem  25014  preotr1  25337  fldax3  25533  fldax4  25534  fldax5  25535  vecax2  25557  icccon3  25804  coda  25832  dualalg  25885  dualded  25886  dehm  25895  iddvvidd  25941  idcvvidc  25942  ivthALT  26361  heiborlem3  26640  iccbnd  26667  rngohom1  26702  idl0cl  26746  maxidlnr  26770  pmtrfinv  27505  stoweidlem11  27863  stoweidlem31  27883  stoweidlem36  27888  stoweidlem38  27890  stoweidlem44  27896  stoweidlem62  27914  sigardiv  27954  sigarcol  27957  sharhght  27958  sigaradd  27959  cevathlem1  27960  cevathlem2  27961  cevath  27962  wlkonwlk  28334  constr3pth  28406  lshpne  29794  opococ  30007  opexmid  30019  hlclat  30170  lclkrslem2  32350
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