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  7627  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  lelttrdi  8756  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccgelb  10345  iccss2  10357  icodisj  10405  ioom  10706  elicore  10712  flqdiv  10773  mulqaddmodid  10816  modsumfzodifsn  10848  addmodlteq  10850  immul  11660  sumtp  12200  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  ballotfilemcdc  13275  ballotfilemfc0  13284  ballotfilemro  13318  ctiunct  13383  structn0fun  13417  strleund  13510  strext  13512  mhmlin  13827  subm0cl  13838  eqger  14080  eqgcpbl  14084  lmodvsdi  14732  lss0cl  14790  rnglidlmsgrp  14918  2idlcpblrng  14944  lmcl  15437  lmtopcnp  15442  xmeter  15628  tgqioo  15747  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limcresi  15858  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  cosordlem  16043  birthdaylem3  16193  perfectlem2  16266  subgruhgredgdm  16682  subumgredg2en  16683  wlkp  16746  wlkpg  16747  wlkvtxiedg  16757  wlk1walkdom  16771  upgr2wlkdc  16789  isclwwlkn  16825  clwwlknwrd  16826  clwwlknon  16841  clwwlknonex2e  16852  trlsegvdeglem3  16874  trlsegvdeglem5  16876  eupth2lem3fi  16888  depindlem2  16919  depindlem3  16920  depind  16921