Theorem simp3d 1038

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1026	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜃)

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  6842  resixp  6967  exmidapne  7570  addcanprleml  7925  addcanprlemu  7926  ltmprr  7953  lelttrdi  8696  ixxdisj  10232  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccsupr  10295  icodisj  10321  ioom  10616  elicore  10622  intfracq  10678  flqdiv  10679  mulqaddmodid  10722  modsumfzodifsn  10754  seqf1oglem2  10878  cjmul  11563  sumtp  12093  crth  12914  eulerthlem1  12917  eulerthlemh  12921  eulerthlemth  12922  4sqlem13m  13094  ennnfonelemim  13164  ctiunct  13180  strsetsid  13234  strleund  13305  strext  13307  mhm0  13670  submcl  13681  submmnd  13682  eqger  13930  eqgcpbl  13934  lmodvsdir  14447  lssclg  14499  rnglidlmsgrp  14632  2idlcpblrng  14658  lmcvg  15069  lmff  15101  lmtopcnp  15102  xmeter  15288  xmetresbl  15292  tgqioo  15407  ivthinclemlopn  15488  ivthinclemuopn  15490  limccl  15511  limcdifap  15514  limcresi  15518  limccnpcntop  15527  limccnp2lem  15528  limccnp2cntop  15529  limccoap  15530  cosordlem  15701  relogbval  15803  relogbzcl  15804  nnlogbexp  15811  mersenne  15852  perfectlem2  15855  subgruhgredgdm  16252  wlk1walkdom  16341  upgr2wlkdc  16359  clwwlknon  16411  clwwlknonex2lem2  16420  depindlem2  16489  depindlem3  16490  depind  16491