Theorem pm2.21d 624

Description: A contradiction implies anything. Deduction from pm2.21 622. (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 622	. 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 620

This theorem is referenced by:  pm2.21dd  625  pm5.21  703  2falsed  710  mtord  791  prlem1  982  eq0rdv  3541  csbprc  3542  rzal  3594  poirr2  5136  nnsucuniel  6706  nnawordex  6740  swoord2  6775  difinfsnlem  7341  exmidomni  7384  elni2  7577  cauappcvgprlemdisj  7914  caucvgprlemdisj  7937  caucvgprprlemdisj  7965  caucvgsr  8065  lelttr  8310  nnsub  9224  nn0ge2m1nn  9506  elnnz  9533  elnn0z  9536  indstr  9871  indstr2  9887  xrltnsym  10072  xrlttr  10074  xrltso  10075  xrlelttr  10085  xltnegi  10114  xsubge0  10160  ixxdisj  10182  icodisj  10271  fzm1  10380  qbtwnxr  10563  frec2uzlt2d  10712  nn0ltexp2  11017  facdiv  11046  resqrexlemgt0  11643  climuni  11916  fsumcl2lem  12022  dvdsle  12468  prmdvdsexpr  12785  prmfac1  12787  sqrt2irr  12797  phibndlem  12851  dvdsprmpweqle  12973  isxmet2d  15142  lgsdir2lem2  15831  lgseisenlem2  15873  wlkv0  16293  trilpolemres  16757