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  7343  addcanprleml  7698  addcanprlemu  7699  ltmprr  7726  lelttrdi  8470  ixxdisj  9995  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccgelb  10024  iccss2  10036  icodisj  10084  ioom  10367  elicore  10373  flqdiv  10430  mulqaddmodid  10473  modsumfzodifsn  10505  addmodlteq  10507  immul  11061  sumtp  11596  crth  12417  phimullem  12418  eulerthlem1  12420  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  ctiunct  12682  structn0fun  12716  strleund  12806  strext  12808  mhmlin  13169  subm0cl  13180  eqger  13430  eqgcpbl  13434  lmodvsdi  13943  lss0cl  14001  rnglidlmsgrp  14129  2idlcpblrng  14155  lmcl  14565  lmtopcnp  14570  xmeter  14756  tgqioo  14875  ivthinclemlopn  14956  ivthinclemuopn  14958  limcimolemlt  14984  limcresi  14986  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  cosordlem  15169  perfectlem2  15320