Theorem simp2d 1041

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp2bi  1044  erinxp  6887  resixp  7020  exmidapne  7633  addcanprleml  7988  addcanprlemu  7989  ltmprr  8016  lelttrdi  8762  ixxdisj  10323  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccgelb  10352  iccss2  10364  icodisj  10412  ioom  10713  elicore  10719  flqdiv  10780  mulqaddmodid  10823  modsumfzodifsn  10855  addmodlteq  10857  immul  11667  sumtp  12207  crth  13032  phimullem  13033  eulerthlem1  13035  eulerthlema  13038  eulerthlemh  13039  eulerthlemth  13040  ballotfilemcdc  13282  ballotfilemfc0  13291  ballotfilemro  13325  ctiunct  13390  structn0fun  13424  strleund  13517  strext  13519  mhmlin  13834  subm0cl  13845  eqger  14087  eqgcpbl  14091  lmodvsdi  14758  lss0cl  14816  rnglidlmsgrp  14944  2idlcpblrng  14970  lmcl  15483  lmtopcnp  15488  xmeter  15674  tgqioo  15793  ivthinclemlopn  15874  ivthinclemuopn  15876  limcimolemlt  15902  limcresi  15904  limccnpcntop  15913  limccnp2lem  15914  limccnp2cntop  15915  cosordlem  16089  birthdaylem3  16239  perfectlem2  16312  subgruhgredgdm  16728  subumgredg2en  16729  wlkp  16792  wlkpg  16793  wlkvtxiedg  16803  wlk1walkdom  16817  upgr2wlkdc  16835  isclwwlkn  16871  clwwlknwrd  16872  clwwlknon  16887  clwwlknonex2e  16898  trlsegvdeglem3  16920  trlsegvdeglem5  16922  eupth2lem3fi  16934  depindlem2  16965  depindlem3  16966  depind  16967