Theorem simp3d 1035

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp3bi  1038  erinxp  6769  resixp  6893  exmidapne  7462  addcanprleml  7817  addcanprlemu  7818  ltmprr  7845  lelttrdi  8589  ixxdisj  10116  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccsupr  10179  icodisj  10205  ioom  10497  elicore  10503  intfracq  10559  flqdiv  10560  mulqaddmodid  10603  modsumfzodifsn  10635  seqf1oglem2  10759  cjmul  11417  sumtp  11946  crth  12767  eulerthlem1  12770  eulerthlemh  12774  eulerthlemth  12775  4sqlem13m  12947  ennnfonelemim  13016  ctiunct  13032  strsetsid  13086  strleund  13157  strext  13159  mhm0  13522  submcl  13533  submmnd  13534  eqger  13782  eqgcpbl  13786  lmodvsdir  14297  lssclg  14349  rnglidlmsgrp  14482  2idlcpblrng  14508  lmcvg  14912  lmff  14944  lmtopcnp  14945  xmeter  15131  xmetresbl  15135  tgqioo  15250  ivthinclemlopn  15331  ivthinclemuopn  15333  limccl  15354  limcdifap  15357  limcresi  15361  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  limccoap  15373  cosordlem  15544  relogbval  15646  relogbzcl  15647  nnlogbexp  15654  mersenne  15692  perfectlem2  15695  wlk1walkdom  16131  upgr2wlkdc  16147