Theorem simp3d 1035

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp3bi  1038  erinxp  6764  resixp  6888  exmidapne  7454  addcanprleml  7809  addcanprlemu  7810  ltmprr  7837  lelttrdi  8581  ixxdisj  10107  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccsupr  10170  icodisj  10196  ioom  10488  elicore  10494  intfracq  10550  flqdiv  10551  mulqaddmodid  10594  modsumfzodifsn  10626  seqf1oglem2  10750  cjmul  11404  sumtp  11933  crth  12754  eulerthlem1  12757  eulerthlemh  12761  eulerthlemth  12762  4sqlem13m  12934  ennnfonelemim  13003  ctiunct  13019  strsetsid  13073  strleund  13144  strext  13146  mhm0  13509  submcl  13520  submmnd  13521  eqger  13769  eqgcpbl  13773  lmodvsdir  14284  lssclg  14336  rnglidlmsgrp  14469  2idlcpblrng  14495  lmcvg  14899  lmff  14931  lmtopcnp  14932  xmeter  15118  xmetresbl  15122  tgqioo  15237  ivthinclemlopn  15318  ivthinclemuopn  15320  limccl  15341  limcdifap  15344  limcresi  15348  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  limccoap  15360  cosordlem  15531  relogbval  15633  relogbzcl  15634  nnlogbexp  15641  mersenne  15679  perfectlem2  15682  wlk1walkdom  16080  upgr2wlkdc  16096