Theorem pm2.21d 620

Description: A contradiction implies anything. Deduction from pm2.21 618. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
pm2.21d	|- ( ph -> ( ps -> ch ) )

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 |- ( ph -> -. ps )
2		pm2.21 618	. 2 |- ( -. ps -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 616

This theorem is referenced by:  pm2.21dd  621  pm5.21  696  2falsed  703  mtord  784  prlem1  975  eq0rdv  3492  csbprc  3493  rzal  3545  poirr2  5059  nnsucuniel  6550  nnawordex  6584  swoord2  6619  difinfsnlem  7160  exmidomni  7203  elni2  7376  cauappcvgprlemdisj  7713  caucvgprlemdisj  7736  caucvgprprlemdisj  7764  caucvgsr  7864  lelttr  8110  nnsub  9023  nn0ge2m1nn  9303  elnnz  9330  elnn0z  9333  indstr  9661  indstr2  9677  xrltnsym  9862  xrlttr  9864  xrltso  9865  xrlelttr  9875  xltnegi  9904  xsubge0  9950  ixxdisj  9972  icodisj  10061  fzm1  10169  qbtwnxr  10329  frec2uzlt2d  10478  nn0ltexp2  10783  facdiv  10812  resqrexlemgt0  11167  climuni  11439  fsumcl2lem  11544  dvdsle  11989  prmdvdsexpr  12291  prmfac1  12293  sqrt2irr  12303  phibndlem  12357  dvdsprmpweqle  12478  isxmet2d  14527  lgsdir2lem2  15186  lgseisenlem2  15228  trilpolemres  15602