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  6773  resixp  6897  exmidapne  7472  addcanprleml  7827  addcanprlemu  7828  ltmprr  7855  lelttrdi  8599  ixxdisj  10131  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccsupr  10194  icodisj  10220  ioom  10513  elicore  10519  intfracq  10575  flqdiv  10576  mulqaddmodid  10619  modsumfzodifsn  10651  seqf1oglem2  10775  cjmul  11439  sumtp  11968  crth  12789  eulerthlem1  12792  eulerthlemh  12796  eulerthlemth  12797  4sqlem13m  12969  ennnfonelemim  13038  ctiunct  13054  strsetsid  13108  strleund  13179  strext  13181  mhm0  13544  submcl  13555  submmnd  13556  eqger  13804  eqgcpbl  13808  lmodvsdir  14319  lssclg  14371  rnglidlmsgrp  14504  2idlcpblrng  14530  lmcvg  14934  lmff  14966  lmtopcnp  14967  xmeter  15153  xmetresbl  15157  tgqioo  15272  ivthinclemlopn  15353  ivthinclemuopn  15355  limccl  15376  limcdifap  15379  limcresi  15383  limccnpcntop  15392  limccnp2lem  15393  limccnp2cntop  15394  limccoap  15395  cosordlem  15566  relogbval  15668  relogbzcl  15669  nnlogbexp  15676  mersenne  15714  perfectlem2  15717  wlk1walkdom  16170  upgr2wlkdc  16186  clwwlknon  16238  clwwlknonex2lem2  16247