Theorem simprd 449

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) A translation of natural deduction rule /\ ER (/\ elimination right), see natded in set.mm. (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
simprd.1	|- (ph -> (ps /\ ch))

Assertion

Ref	Expression
simprd	|- (ph -> ch)

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. . 3 |- (ph -> (ps /\ ch))
2	1	ancomd 438	. 2 |- (ph -> (ch /\ ps))
3	2	simpld 445	1 |- (ph -> ch)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  simprbi  450  simplbda  607  simp2  956  simp3  957  nic-mp  1436  nic-mpALT  1437  unssbd  3442  ncfindi  4476  ncfinsn  4477  ncfineleq  4478  ncfintfin  4496  tfinltfinlem1  4501  evennnul  4509  oddnnul  4510  1cvsfin  4543  vfintle  4547  vfin1cltv  4548  vfinncvntnn  4549  vfinspsslem1  4551  vfinncsp  4555  brrelrnex  4692  elima  4755  vtoclr  4817  brco  4884  brres  4950  elimasn  5020  feu  5243  fun11iun  5306  fv3  5342  opbr1st  5502  opbr2nd  5503  ndmovord  5621  caovmo  5646  elovex2  5651  brfns  5834  fnfullfunlem1  5857  frds  5936  brltc  6115  eqncg  6127  nmembers1lem3  6271  spacind  6288  nchoicelem3  6292  nchoicelem5  6294  nchoice  6309