Theorem simp3d 1042

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
simp3d	|- ( ph -> th )

Proof of Theorem simp3d

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

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  ax-ia3 108

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

This theorem is used by:  simp3bi  1045  erinxp  6883  resixp  7015  exmidapne  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8754  ixxdisj  10305  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccsupr  10368  icodisj  10394  ioom  10695  elicore  10701  intfracq  10757  flqdiv  10758  mulqaddmodid  10801  modsumfzodifsn  10833  seqf1oglem2  10957  cjmul  11650  sumtp  12181  crth  13002  eulerthlem1  13005  eulerthlemh  13009  eulerthlemth  13010  4sqlem13m  13182  ballotfilemro  13266  ennnfonelemim  13315  ctiunct  13331  strsetsid  13385  strleund  13457  strext  13459  mhm0  13775  submcl  13786  submmnd  13787  eqger  14027  eqgcpbl  14031  lmodvsdir  14649  lssclg  14701  rnglidlmsgrp  14834  2idlcpblrng  14860  lmcvg  15318  lmff  15350  lmtopcnp  15351  xmeter  15537  xmetresbl  15541  tgqioo  15656  ivthinclemlopn  15737  ivthinclemuopn  15739  limccl  15760  limcdifap  15763  limcresi  15767  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  limccoap  15779  cosordlem  15950  relogbval  16053  relogbzcl  16054  nnlogbexp  16061  birthdaylem3  16089  mersenne  16111  perfectlem2  16114  subgruhgredgdm  16511  wlk1walkdom  16600  upgr2wlkdc  16618  clwwlknon  16670  clwwlknonex2lem2  16679  depindlem2  16748  depindlem3  16749  depind  16750