Theorem simp2d 1041

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

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp2 1029	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp2bi  1044  erinxp  6883  resixp  7015  exmidapne  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8754  ixxdisj  10305  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccgelb  10334  iccss2  10346  icodisj  10394  ioom  10695  elicore  10701  flqdiv  10758  mulqaddmodid  10801  modsumfzodifsn  10833  addmodlteq  10835  immul  11644  sumtp  12181  crth  13002  phimullem  13003  eulerthlem1  13005  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  ballotfilemcdc  13223  ballotfilemfc0  13232  ballotfilemro  13266  ctiunct  13331  structn0fun  13365  strleund  13457  strext  13459  mhmlin  13774  subm0cl  13785  eqger  14027  eqgcpbl  14031  lmodvsdi  14648  lss0cl  14706  rnglidlmsgrp  14834  2idlcpblrng  14860  lmcl  15346  lmtopcnp  15351  xmeter  15537  tgqioo  15656  ivthinclemlopn  15737  ivthinclemuopn  15739  limcimolemlt  15765  limcresi  15767  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  cosordlem  15950  birthdaylem3  16089  perfectlem2  16114  subgruhgredgdm  16511  subumgredg2en  16512  wlkp  16575  wlkpg  16576  wlkvtxiedg  16586  wlk1walkdom  16600  upgr2wlkdc  16618  isclwwlkn  16654  clwwlknwrd  16655  clwwlknon  16670  clwwlknonex2e  16681  trlsegvdeglem3  16703  trlsegvdeglem5  16705  eupth2lem3fi  16717  depindlem2  16748  depindlem3  16749  depind  16750