Theorem simp3d 1037

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp3bi  1040  erinxp  6778  resixp  6902  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccsupr  10201  icodisj  10227  ioom  10521  elicore  10527  intfracq  10583  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  seqf1oglem2  10783  cjmul  11447  sumtp  11977  crth  12798  eulerthlem1  12801  eulerthlemh  12805  eulerthlemth  12806  4sqlem13m  12978  ennnfonelemim  13047  ctiunct  13063  strsetsid  13117  strleund  13188  strext  13190  mhm0  13553  submcl  13564  submmnd  13565  eqger  13813  eqgcpbl  13817  lmodvsdir  14329  lssclg  14381  rnglidlmsgrp  14514  2idlcpblrng  14540  lmcvg  14944  lmff  14976  lmtopcnp  14977  xmeter  15163  xmetresbl  15167  tgqioo  15282  ivthinclemlopn  15363  ivthinclemuopn  15365  limccl  15386  limcdifap  15389  limcresi  15393  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  limccoap  15405  cosordlem  15576  relogbval  15678  relogbzcl  15679  nnlogbexp  15686  mersenne  15724  perfectlem2  15727  subgruhgredgdm  16124  wlk1walkdom  16213  upgr2wlkdc  16231  clwwlknon  16283  clwwlknonex2lem2  16292  depindlem2  16347  depindlem3  16348  depind  16349