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  3495  csbprc  3496  rzal  3548  poirr2  5062  nnsucuniel  6553  nnawordex  6587  swoord2  6622  difinfsnlem  7165  exmidomni  7208  elni2  7381  cauappcvgprlemdisj  7718  caucvgprlemdisj  7741  caucvgprprlemdisj  7769  caucvgsr  7869  lelttr  8115  nnsub  9029  nn0ge2m1nn  9309  elnnz  9336  elnn0z  9339  indstr  9667  indstr2  9683  xrltnsym  9868  xrlttr  9870  xrltso  9871  xrlelttr  9881  xltnegi  9910  xsubge0  9956  ixxdisj  9978  icodisj  10067  fzm1  10175  qbtwnxr  10347  frec2uzlt2d  10496  nn0ltexp2  10801  facdiv  10830  resqrexlemgt0  11185  climuni  11458  fsumcl2lem  11563  dvdsle  12009  prmdvdsexpr  12318  prmfac1  12320  sqrt2irr  12330  phibndlem  12384  dvdsprmpweqle  12506  isxmet2d  14584  lgsdir2lem2  15270  lgseisenlem2  15312  trilpolemres  15686