Theorem simp2d 1012

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp2bi  1015  erinxp  6677  resixp  6801  exmidapne  7345  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  lelttrdi  8472  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccgelb  10026  iccss2  10038  icodisj  10086  ioom  10369  elicore  10375  flqdiv  10432  mulqaddmodid  10475  modsumfzodifsn  10507  addmodlteq  10509  immul  11063  sumtp  11598  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  ctiunct  12684  structn0fun  12718  strleund  12808  strext  12810  mhmlin  13171  subm0cl  13182  eqger  13432  eqgcpbl  13436  lmodvsdi  13945  lss0cl  14003  rnglidlmsgrp  14131  2idlcpblrng  14157  lmcl  14567  lmtopcnp  14572  xmeter  14758  tgqioo  14877  ivthinclemlopn  14958  ivthinclemuopn  14960  limcimolemlt  14986  limcresi  14988  limccnpcntop  14997  limccnp2lem  14998  limccnp2cntop  14999  cosordlem  15171  perfectlem2  15322