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  6764  resixp  6888  exmidapne  7454  addcanprleml  7809  addcanprlemu  7810  ltmprr  7837  lelttrdi  8581  ixxdisj  10107  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccgelb  10136  iccss2  10148  icodisj  10196  ioom  10488  elicore  10494  flqdiv  10551  mulqaddmodid  10594  modsumfzodifsn  10626  addmodlteq  10628  immul  11398  sumtp  11933  crth  12754  phimullem  12755  eulerthlem1  12757  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  ctiunct  13019  structn0fun  13053  strleund  13144  strext  13146  mhmlin  13508  subm0cl  13519  eqger  13769  eqgcpbl  13773  lmodvsdi  14283  lss0cl  14341  rnglidlmsgrp  14469  2idlcpblrng  14495  lmcl  14927  lmtopcnp  14932  xmeter  15118  tgqioo  15237  ivthinclemlopn  15318  ivthinclemuopn  15320  limcimolemlt  15346  limcresi  15348  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  cosordlem  15531  perfectlem2  15682  wlkp  16055  wlkpg  16056  wlkvtxiedg  16066  wlk1walkdom  16080  upgr2wlkdc  16096