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  8755  ixxdisj  10315  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccgelb  10344  iccss2  10356  icodisj  10404  ioom  10705  elicore  10711  flqdiv  10771  mulqaddmodid  10814  modsumfzodifsn  10846  addmodlteq  10848  immul  11658  sumtp  12197  crth  13022  phimullem  13023  eulerthlem1  13025  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  ballotfilemcdc  13272  ballotfilemfc0  13281  ballotfilemro  13315  ctiunct  13380  structn0fun  13414  strleund  13506  strext  13508  mhmlin  13823  subm0cl  13834  eqger  14076  eqgcpbl  14080  lmodvsdi  14697  lss0cl  14755  rnglidlmsgrp  14883  2idlcpblrng  14909  lmcl  15395  lmtopcnp  15400  xmeter  15586  tgqioo  15705  ivthinclemlopn  15786  ivthinclemuopn  15788  limcimolemlt  15814  limcresi  15816  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  cosordlem  16000  birthdaylem3  16146  perfectlem2  16198  subgruhgredgdm  16609  subumgredg2en  16610  wlkp  16673  wlkpg  16674  wlkvtxiedg  16684  wlk1walkdom  16698  upgr2wlkdc  16716  isclwwlkn  16752  clwwlknwrd  16753  clwwlknon  16768  clwwlknonex2e  16779  trlsegvdeglem3  16801  trlsegvdeglem5  16803  eupth2lem3fi  16815  depindlem2  16846  depindlem3  16847  depind  16848