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  6856  resixp  6981  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8718  ixxdisj  10258  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccsupr  10321  icodisj  10347  ioom  10647  elicore  10653  intfracq  10709  flqdiv  10710  mulqaddmodid  10753  modsumfzodifsn  10785  seqf1oglem2  10909  cjmul  11598  sumtp  12128  crth  12949  eulerthlem1  12952  eulerthlemh  12956  eulerthlemth  12957  4sqlem13m  13129  ballotfilemro  13213  ennnfonelemim  13262  ctiunct  13278  strsetsid  13332  strleund  13403  strext  13405  mhm0  13726  submcl  13737  submmnd  13738  eqger  13980  eqgcpbl  13984  lmodvsdir  14589  lssclg  14641  rnglidlmsgrp  14774  2idlcpblrng  14800  lmcvg  15211  lmff  15243  lmtopcnp  15244  xmeter  15430  xmetresbl  15434  tgqioo  15549  ivthinclemlopn  15630  ivthinclemuopn  15632  limccl  15653  limcdifap  15656  limcresi  15660  limccnpcntop  15669  limccnp2lem  15670  limccnp2cntop  15671  limccoap  15672  cosordlem  15843  relogbval  15945  relogbzcl  15946  nnlogbexp  15953  mersenne  15994  perfectlem2  15997  subgruhgredgdm  16394  wlk1walkdom  16483  upgr2wlkdc  16501  clwwlknon  16553  clwwlknonex2lem2  16562  depindlem2  16631  depindlem3  16632  depind  16633