Theorem simp3d 1013

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp3bi  1016  erinxp  6669  resixp  6793  exmidapne  7329  addcanprleml  7683  addcanprlemu  7684  ltmprr  7711  lelttrdi  8455  ixxdisj  9980  ixxss1  9981  ixxss2  9982  ixxss12  9983  iccsupr  10043  icodisj  10069  ioom  10352  elicore  10358  intfracq  10414  flqdiv  10415  mulqaddmodid  10458  modsumfzodifsn  10490  seqf1oglem2  10614  cjmul  11052  sumtp  11581  crth  12402  eulerthlem1  12405  eulerthlemh  12409  eulerthlemth  12410  4sqlem13m  12582  ennnfonelemim  12651  ctiunct  12667  strsetsid  12721  strleund  12791  strext  12793  mhm0  13110  submcl  13121  submmnd  13122  eqger  13364  eqgcpbl  13368  lmodvsdir  13878  lssclg  13930  rnglidlmsgrp  14063  2idlcpblrng  14089  lmcvg  14463  lmff  14495  lmtopcnp  14496  xmeter  14682  xmetresbl  14686  tgqioo  14801  ivthinclemlopn  14882  ivthinclemuopn  14884  limccl  14905  limcdifap  14908  limcresi  14912  limccnpcntop  14921  limccnp2lem  14922  limccnp2cntop  14923  limccoap  14924  cosordlem  15095  relogbval  15197  relogbzcl  15198  nnlogbexp  15205  mersenne  15243  perfectlem2  15246