Theorem simp2d 1037

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp2bi  1040  erinxp  6842  resixp  6967  exmidapne  7570  addcanprleml  7925  addcanprlemu  7926  ltmprr  7953  lelttrdi  8696  ixxdisj  10232  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccgelb  10261  iccss2  10273  icodisj  10321  ioom  10616  elicore  10622  flqdiv  10679  mulqaddmodid  10722  modsumfzodifsn  10754  addmodlteq  10756  immul  11557  sumtp  12093  crth  12914  phimullem  12915  eulerthlem1  12917  eulerthlema  12920  eulerthlemh  12921  eulerthlemth  12922  ctiunct  13180  structn0fun  13214  strleund  13305  strext  13307  mhmlin  13669  subm0cl  13680  eqger  13930  eqgcpbl  13934  lmodvsdi  14446  lss0cl  14504  rnglidlmsgrp  14632  2idlcpblrng  14658  lmcl  15097  lmtopcnp  15102  xmeter  15288  tgqioo  15407  ivthinclemlopn  15488  ivthinclemuopn  15490  limcimolemlt  15516  limcresi  15518  limccnpcntop  15527  limccnp2lem  15528  limccnp2cntop  15529  cosordlem  15701  perfectlem2  15855  subgruhgredgdm  16252  subumgredg2en  16253  wlkp  16316  wlkpg  16317  wlkvtxiedg  16327  wlk1walkdom  16341  upgr2wlkdc  16359  isclwwlkn  16395  clwwlknwrd  16396  clwwlknon  16411  clwwlknonex2e  16422  trlsegvdeglem3  16444  trlsegvdeglem5  16446  eupth2lem3fi  16458  depindlem2  16489  depindlem3  16490  depind  16491