Theorem simp2d 1034

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2d	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp2 1022	. 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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simp2bi  1037  erinxp  6773  resixp  6897  exmidapne  7472  addcanprleml  7827  addcanprlemu  7828  ltmprr  7855  lelttrdi  8599  ixxdisj  10131  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccgelb  10160  iccss2  10172  icodisj  10220  ioom  10513  elicore  10519  flqdiv  10576  mulqaddmodid  10619  modsumfzodifsn  10651  addmodlteq  10653  immul  11433  sumtp  11968  crth  12789  phimullem  12790  eulerthlem1  12792  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  ctiunct  13054  structn0fun  13088  strleund  13179  strext  13181  mhmlin  13543  subm0cl  13554  eqger  13804  eqgcpbl  13808  lmodvsdi  14318  lss0cl  14376  rnglidlmsgrp  14504  2idlcpblrng  14530  lmcl  14962  lmtopcnp  14967  xmeter  15153  tgqioo  15272  ivthinclemlopn  15353  ivthinclemuopn  15355  limcimolemlt  15381  limcresi  15383  limccnpcntop  15392  limccnp2lem  15393  limccnp2cntop  15394  cosordlem  15566  perfectlem2  15717  wlkp  16145  wlkpg  16146  wlkvtxiedg  16156  wlk1walkdom  16170  upgr2wlkdc  16186  isclwwlkn  16222  clwwlknwrd  16223  clwwlknon  16238  clwwlknonex2e  16249