Theorem simp3d 1016

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

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  simp3bi  1019  erinxp  6726  resixp  6850  exmidapne  7414  addcanprleml  7769  addcanprlemu  7770  ltmprr  7797  lelttrdi  8541  ixxdisj  10067  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccsupr  10130  icodisj  10156  ioom  10447  elicore  10453  intfracq  10509  flqdiv  10510  mulqaddmodid  10553  modsumfzodifsn  10585  seqf1oglem2  10709  cjmul  11362  sumtp  11891  crth  12712  eulerthlem1  12715  eulerthlemh  12719  eulerthlemth  12720  4sqlem13m  12892  ennnfonelemim  12961  ctiunct  12977  strsetsid  13031  strleund  13102  strext  13104  mhm0  13467  submcl  13478  submmnd  13479  eqger  13727  eqgcpbl  13731  lmodvsdir  14241  lssclg  14293  rnglidlmsgrp  14426  2idlcpblrng  14452  lmcvg  14856  lmff  14888  lmtopcnp  14889  xmeter  15075  xmetresbl  15079  tgqioo  15194  ivthinclemlopn  15275  ivthinclemuopn  15277  limccl  15298  limcdifap  15301  limcresi  15305  limccnpcntop  15314  limccnp2lem  15315  limccnp2cntop  15316  limccoap  15317  cosordlem  15488  relogbval  15590  relogbzcl  15591  nnlogbexp  15598  mersenne  15636  perfectlem2  15639