Theorem simp3d 1014

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp3bi  1017  erinxp  6703  resixp  6827  exmidapne  7379  addcanprleml  7734  addcanprlemu  7735  ltmprr  7762  lelttrdi  8506  ixxdisj  10032  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccsupr  10095  icodisj  10121  ioom  10410  elicore  10416  intfracq  10472  flqdiv  10473  mulqaddmodid  10516  modsumfzodifsn  10548  seqf1oglem2  10672  cjmul  11240  sumtp  11769  crth  12590  eulerthlem1  12593  eulerthlemh  12597  eulerthlemth  12598  4sqlem13m  12770  ennnfonelemim  12839  ctiunct  12855  strsetsid  12909  strleund  12979  strext  12981  mhm0  13344  submcl  13355  submmnd  13356  eqger  13604  eqgcpbl  13608  lmodvsdir  14118  lssclg  14170  rnglidlmsgrp  14303  2idlcpblrng  14329  lmcvg  14733  lmff  14765  lmtopcnp  14766  xmeter  14952  xmetresbl  14956  tgqioo  15071  ivthinclemlopn  15152  ivthinclemuopn  15154  limccl  15175  limcdifap  15178  limcresi  15182  limccnpcntop  15191  limccnp2lem  15192  limccnp2cntop  15193  limccoap  15194  cosordlem  15365  relogbval  15467  relogbzcl  15468  nnlogbexp  15475  mersenne  15513  perfectlem2  15516