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  6821  resixp  6945  exmidapne  7522  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  lelttrdi  8649  ixxdisj  10181  ixxss1  10182  ixxss2  10183  ixxss12  10184  iccsupr  10244  icodisj  10270  ioom  10564  elicore  10570  intfracq  10626  flqdiv  10627  mulqaddmodid  10670  modsumfzodifsn  10702  seqf1oglem2  10826  cjmul  11506  sumtp  12036  crth  12857  eulerthlem1  12860  eulerthlemh  12864  eulerthlemth  12865  4sqlem13m  13037  ennnfonelemim  13106  ctiunct  13122  strsetsid  13176  strleund  13247  strext  13249  mhm0  13612  submcl  13623  submmnd  13624  eqger  13872  eqgcpbl  13876  lmodvsdir  14388  lssclg  14440  rnglidlmsgrp  14573  2idlcpblrng  14599  lmcvg  15008  lmff  15040  lmtopcnp  15041  xmeter  15227  xmetresbl  15231  tgqioo  15346  ivthinclemlopn  15427  ivthinclemuopn  15429  limccl  15450  limcdifap  15453  limcresi  15457  limccnpcntop  15466  limccnp2lem  15467  limccnp2cntop  15468  limccoap  15469  cosordlem  15640  relogbval  15742  relogbzcl  15743  nnlogbexp  15750  mersenne  15788  perfectlem2  15791  subgruhgredgdm  16188  wlk1walkdom  16277  upgr2wlkdc  16295  clwwlknon  16347  clwwlknonex2lem2  16356  depindlem2  16425  depindlem3  16426  depind  16427