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  6883  resixp  7015  exmidapne  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8754  ixxdisj  10307  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccgelb  10336  iccss2  10348  icodisj  10396  ioom  10697  elicore  10703  flqdiv  10760  mulqaddmodid  10803  modsumfzodifsn  10835  addmodlteq  10837  immul  11646  sumtp  12183  crth  13004  phimullem  13005  eulerthlem1  13007  eulerthlema  13010  eulerthlemh  13011  eulerthlemth  13012  ballotfilemcdc  13225  ballotfilemfc0  13234  ballotfilemro  13268  ctiunct  13333  structn0fun  13367  strleund  13459  strext  13461  mhmlin  13776  subm0cl  13787  eqger  14029  eqgcpbl  14033  lmodvsdi  14650  lss0cl  14708  rnglidlmsgrp  14836  2idlcpblrng  14862  lmcl  15348  lmtopcnp  15353  xmeter  15539  tgqioo  15658  ivthinclemlopn  15739  ivthinclemuopn  15741  limcimolemlt  15767  limcresi  15769  limccnpcntop  15778  limccnp2lem  15779  limccnp2cntop  15780  cosordlem  15953  birthdaylem3  16095  perfectlem2  16120  subgruhgredgdm  16523  subumgredg2en  16524  wlkp  16587  wlkpg  16588  wlkvtxiedg  16598  wlk1walkdom  16612  upgr2wlkdc  16630  isclwwlkn  16666  clwwlknwrd  16667  clwwlknon  16682  clwwlknonex2e  16693  trlsegvdeglem3  16715  trlsegvdeglem5  16717  eupth2lem3fi  16729  depindlem2  16760  depindlem3  16761  depind  16762