Theorem simp2d 1036

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp2bi  1039  erinxp  6783  resixp  6907  exmidapne  7484  addcanprleml  7839  addcanprlemu  7840  ltmprr  7867  lelttrdi  8611  ixxdisj  10143  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccgelb  10172  iccss2  10184  icodisj  10232  ioom  10526  elicore  10532  flqdiv  10589  mulqaddmodid  10632  modsumfzodifsn  10664  addmodlteq  10666  immul  11462  sumtp  11998  crth  12819  phimullem  12820  eulerthlem1  12822  eulerthlema  12825  eulerthlemh  12826  eulerthlemth  12827  ctiunct  13084  structn0fun  13118  strleund  13209  strext  13211  mhmlin  13573  subm0cl  13584  eqger  13834  eqgcpbl  13838  lmodvsdi  14349  lss0cl  14407  rnglidlmsgrp  14535  2idlcpblrng  14561  lmcl  14998  lmtopcnp  15003  xmeter  15189  tgqioo  15308  ivthinclemlopn  15389  ivthinclemuopn  15391  limcimolemlt  15417  limcresi  15419  limccnpcntop  15428  limccnp2lem  15429  limccnp2cntop  15430  cosordlem  15602  perfectlem2  15753  subgruhgredgdm  16150  subumgredg2en  16151  wlkp  16214  wlkpg  16215  wlkvtxiedg  16225  wlk1walkdom  16239  upgr2wlkdc  16257  isclwwlkn  16293  clwwlknwrd  16294  clwwlknon  16309  clwwlknonex2e  16320  trlsegvdeglem3  16342  trlsegvdeglem5  16344  eupth2lem3fi  16356  depindlem2  16387  depindlem3  16388  depind  16389