Theorem simp2d 1012

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	|- ( ph -> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
simp2d	|- ( ph -> ch )

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp2 1000	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

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  6636  resixp  6760  exmidapne  7290  addcanprleml  7644  addcanprlemu  7645  ltmprr  7672  lelttrdi  8414  ixxdisj  9935  ixxss1  9936  ixxss2  9937  ixxss12  9938  iccgelb  9964  iccss2  9976  icodisj  10024  ioom  10293  elicore  10299  flqdiv  10354  mulqaddmodid  10397  modsumfzodifsn  10429  addmodlteq  10431  immul  10923  sumtp  11457  crth  12259  phimullem  12260  eulerthlem1  12262  eulerthlema  12265  eulerthlemh  12266  eulerthlemth  12267  ctiunct  12494  structn0fun  12528  strleund  12618  strext  12620  mhmlin  12934  subm0cl  12945  eqger  13180  eqgcpbl  13184  lmodvsdi  13644  lss0cl  13702  rnglidlmsgrp  13830  2idlcpblrng  13855  lmcl  14222  lmtopcnp  14227  xmeter  14413  tgqioo  14524  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimolemlt  14610  limcresi  14612  limccnpcntop  14621  limccnp2lem  14622  limccnp2cntop  14623  cosordlem  14747