Theorem simp2d 1015

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

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  simp2bi  1018  erinxp  6726  resixp  6850  exmidapne  7414  addcanprleml  7769  addcanprlemu  7770  ltmprr  7797  lelttrdi  8541  ixxdisj  10067  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccgelb  10096  iccss2  10108  icodisj  10156  ioom  10447  elicore  10453  flqdiv  10510  mulqaddmodid  10553  modsumfzodifsn  10585  addmodlteq  10587  immul  11356  sumtp  11891  crth  12712  phimullem  12713  eulerthlem1  12715  eulerthlema  12718  eulerthlemh  12719  eulerthlemth  12720  ctiunct  12977  structn0fun  13011  strleund  13102  strext  13104  mhmlin  13466  subm0cl  13477  eqger  13727  eqgcpbl  13731  lmodvsdi  14240  lss0cl  14298  rnglidlmsgrp  14426  2idlcpblrng  14452  lmcl  14884  lmtopcnp  14889  xmeter  15075  tgqioo  15194  ivthinclemlopn  15275  ivthinclemuopn  15277  limcimolemlt  15303  limcresi  15305  limccnpcntop  15314  limccnp2lem  15315  limccnp2cntop  15316  cosordlem  15488  perfectlem2  15639