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  3504  csbprc  3505  rzal  3557  poirr2  5072  nnsucuniel  6571  nnawordex  6605  swoord2  6640  difinfsnlem  7183  exmidomni  7226  elni2  7409  cauappcvgprlemdisj  7746  caucvgprlemdisj  7769  caucvgprprlemdisj  7797  caucvgsr  7897  lelttr  8143  nnsub  9057  nn0ge2m1nn  9337  elnnz  9364  elnn0z  9367  indstr  9696  indstr2  9712  xrltnsym  9897  xrlttr  9899  xrltso  9900  xrlelttr  9910  xltnegi  9939  xsubge0  9985  ixxdisj  10007  icodisj  10096  fzm1  10204  qbtwnxr  10381  frec2uzlt2d  10530  nn0ltexp2  10835  facdiv  10864  resqrexlemgt0  11250  climuni  11523  fsumcl2lem  11628  dvdsle  12074  prmdvdsexpr  12391  prmfac1  12393  sqrt2irr  12403  phibndlem  12457  dvdsprmpweqle  12579  isxmet2d  14738  lgsdir2lem2  15424  lgseisenlem2  15466  trilpolemres  15845