Theorem simp2d 1013

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp2bi  1016  erinxp  6703  resixp  6827  exmidapne  7379  addcanprleml  7734  addcanprlemu  7735  ltmprr  7762  lelttrdi  8506  ixxdisj  10032  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccgelb  10061  iccss2  10073  icodisj  10121  ioom  10410  elicore  10416  flqdiv  10473  mulqaddmodid  10516  modsumfzodifsn  10548  addmodlteq  10550  immul  11234  sumtp  11769  crth  12590  phimullem  12591  eulerthlem1  12593  eulerthlema  12596  eulerthlemh  12597  eulerthlemth  12598  ctiunct  12855  structn0fun  12889  strleund  12979  strext  12981  mhmlin  13343  subm0cl  13354  eqger  13604  eqgcpbl  13608  lmodvsdi  14117  lss0cl  14175  rnglidlmsgrp  14303  2idlcpblrng  14329  lmcl  14761  lmtopcnp  14766  xmeter  14952  tgqioo  15071  ivthinclemlopn  15152  ivthinclemuopn  15154  limcimolemlt  15180  limcresi  15182  limccnpcntop  15191  limccnp2lem  15192  limccnp2cntop  15193  cosordlem  15365  perfectlem2  15516