Theorem simp3d 1037

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp3bi  1040  erinxp  6783  resixp  6907  exmidapne  7484  addcanprleml  7839  addcanprlemu  7840  ltmprr  7867  lelttrdi  8611  ixxdisj  10143  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccsupr  10206  icodisj  10232  ioom  10526  elicore  10532  intfracq  10588  flqdiv  10589  mulqaddmodid  10632  modsumfzodifsn  10664  seqf1oglem2  10788  cjmul  11468  sumtp  11998  crth  12819  eulerthlem1  12822  eulerthlemh  12826  eulerthlemth  12827  4sqlem13m  12999  ennnfonelemim  13068  ctiunct  13084  strsetsid  13138  strleund  13209  strext  13211  mhm0  13574  submcl  13585  submmnd  13586  eqger  13834  eqgcpbl  13838  lmodvsdir  14350  lssclg  14402  rnglidlmsgrp  14535  2idlcpblrng  14561  lmcvg  14970  lmff  15002  lmtopcnp  15003  xmeter  15189  xmetresbl  15193  tgqioo  15308  ivthinclemlopn  15389  ivthinclemuopn  15391  limccl  15412  limcdifap  15415  limcresi  15419  limccnpcntop  15428  limccnp2lem  15429  limccnp2cntop  15430  limccoap  15431  cosordlem  15602  relogbval  15704  relogbzcl  15705  nnlogbexp  15712  mersenne  15750  perfectlem2  15753  subgruhgredgdm  16150  wlk1walkdom  16239  upgr2wlkdc  16257  clwwlknon  16309  clwwlknonex2lem2  16318  depindlem2  16387  depindlem3  16388  depind  16389