Theorem simp3d 1038

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 1026	. 2 |- ( ( ps /\ ch /\ th ) -> th )
3	1, 2	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simp3bi  1041  erinxp  6856  resixp  6981  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8717  ixxdisj  10255  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccsupr  10318  icodisj  10344  ioom  10644  elicore  10650  intfracq  10706  flqdiv  10707  mulqaddmodid  10750  modsumfzodifsn  10782  seqf1oglem2  10906  cjmul  11595  sumtp  12125  crth  12946  eulerthlem1  12949  eulerthlemh  12953  eulerthlemth  12954  4sqlem13m  13126  ballotfilemro  13210  ennnfonelemim  13259  ctiunct  13275  strsetsid  13329  strleund  13400  strext  13402  mhm0  13723  submcl  13734  submmnd  13735  eqger  13977  eqgcpbl  13981  lmodvsdir  14586  lssclg  14638  rnglidlmsgrp  14771  2idlcpblrng  14797  lmcvg  15208  lmff  15240  lmtopcnp  15241  xmeter  15427  xmetresbl  15431  tgqioo  15546  ivthinclemlopn  15627  ivthinclemuopn  15629  limccl  15650  limcdifap  15653  limcresi  15657  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  limccoap  15669  cosordlem  15840  relogbval  15942  relogbzcl  15943  nnlogbexp  15950  mersenne  15991  perfectlem2  15994  subgruhgredgdm  16391  wlk1walkdom  16480  upgr2wlkdc  16498  clwwlknon  16550  clwwlknonex2lem2  16559  depindlem2  16628  depindlem3  16629  depind  16630