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  6769  resixp  6893  exmidapne  7462  addcanprleml  7817  addcanprlemu  7818  ltmprr  7845  lelttrdi  8589  ixxdisj  10116  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccgelb  10145  iccss2  10157  icodisj  10205  ioom  10497  elicore  10503  flqdiv  10560  mulqaddmodid  10603  modsumfzodifsn  10635  addmodlteq  10637  immul  11411  sumtp  11946  crth  12767  phimullem  12768  eulerthlem1  12770  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  ctiunct  13032  structn0fun  13066  strleund  13157  strext  13159  mhmlin  13521  subm0cl  13532  eqger  13782  eqgcpbl  13786  lmodvsdi  14296  lss0cl  14354  rnglidlmsgrp  14482  2idlcpblrng  14508  lmcl  14940  lmtopcnp  14945  xmeter  15131  tgqioo  15250  ivthinclemlopn  15331  ivthinclemuopn  15333  limcimolemlt  15359  limcresi  15361  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  cosordlem  15544  perfectlem2  15695  wlkp  16106  wlkpg  16107  wlkvtxiedg  16117  wlk1walkdom  16131  upgr2wlkdc  16147  clwwlknwrd  16182