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  8755  ixxdisj  10315  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccsupr  10378  icodisj  10404  ioom  10705  elicore  10711  intfracq  10770  flqdiv  10771  mulqaddmodid  10814  modsumfzodifsn  10846  seqf1oglem2  10970  cjmul  11664  sumtp  12197  crth  13022  eulerthlem1  13025  eulerthlemh  13029  eulerthlemth  13030  4sqlem13m  13202  ballotfilemro  13315  ennnfonelemim  13364  ctiunct  13380  strsetsid  13434  strleund  13506  strext  13508  mhm0  13824  submcl  13835  submmnd  13836  eqger  14076  eqgcpbl  14080  lmodvsdir  14698  lssclg  14750  rnglidlmsgrp  14883  2idlcpblrng  14909  lmcvg  15367  lmff  15399  lmtopcnp  15400  xmeter  15586  xmetresbl  15590  tgqioo  15705  ivthinclemlopn  15786  ivthinclemuopn  15788  limccl  15809  limcdifap  15812  limcresi  15816  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  limccoap  15828  cosordlem  16000  relogbval  16106  relogbzcl  16107  nnlogbexp  16114  birthdaylem3  16146  ppiqsval  16156  mersenne  16195  perfectlem2  16198  subgruhgredgdm  16609  wlk1walkdom  16698  upgr2wlkdc  16716  clwwlknon  16768  clwwlknonex2lem2  16777  depindlem2  16846  depindlem3  16847  depind  16848