Theorem simp3d 1042

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  simp3bi  1045  erinxp  6877  resixp  7009  exmidapne  7620  addcanprleml  7975  addcanprlemu  7976  ltmprr  8003  lelttrdi  8748  ixxdisj  10288  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccsupr  10351  icodisj  10377  ioom  10678  elicore  10684  intfracq  10740  flqdiv  10741  mulqaddmodid  10784  modsumfzodifsn  10816  seqf1oglem2  10940  cjmul  11633  sumtp  12164  crth  12985  eulerthlem1  12988  eulerthlemh  12992  eulerthlemth  12993  4sqlem13m  13165  ballotfilemro  13249  ennnfonelemim  13298  ctiunct  13314  strsetsid  13368  strleund  13440  strext  13442  mhm0  13758  submcl  13769  submmnd  13770  eqger  14010  eqgcpbl  14014  lmodvsdir  14632  lssclg  14684  rnglidlmsgrp  14817  2idlcpblrng  14843  lmcvg  15301  lmff  15333  lmtopcnp  15334  xmeter  15520  xmetresbl  15524  tgqioo  15639  ivthinclemlopn  15720  ivthinclemuopn  15722  limccl  15743  limcdifap  15746  limcresi  15750  limccnpcntop  15759  limccnp2lem  15760  limccnp2cntop  15761  limccoap  15762  cosordlem  15933  relogbval  16036  relogbzcl  16037  nnlogbexp  16044  birthdaylem3  16072  mersenne  16094  perfectlem2  16097  subgruhgredgdm  16494  wlk1walkdom  16583  upgr2wlkdc  16601  clwwlknon  16653  clwwlknonex2lem2  16662  depindlem2  16731  depindlem3  16732  depind  16733