Theorem simp3d 1001

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 989	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simp3bi  1004  erinxp  6575  resixp  6699  addcanprleml  7555  addcanprlemu  7556  ltmprr  7583  lelttrdi  8324  ixxdisj  9839  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccsupr  9902  icodisj  9928  ioom  10196  elicore  10202  intfracq  10255  flqdiv  10256  mulqaddmodid  10299  modsumfzodifsn  10331  cjmul  10827  sumtp  11355  crth  12156  eulerthlem1  12159  eulerthlemh  12163  eulerthlemth  12164  ennnfonelemim  12357  ctiunct  12373  strsetsid  12427  strleund  12483  lmcvg  12857  lmff  12889  lmtopcnp  12890  xmeter  13076  xmetresbl  13080  tgqioo  13187  ivthinclemlopn  13254  ivthinclemuopn  13256  limccl  13268  limcdifap  13271  limcresi  13275  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  limccoap  13287  cosordlem  13410  relogbval  13509  relogbzcl  13510  nnlogbexp  13517