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  3491  csbprc  3492  rzal  3544  poirr2  5058  nnsucuniel  6548  nnawordex  6582  swoord2  6617  difinfsnlem  7158  exmidomni  7201  elni2  7374  cauappcvgprlemdisj  7711  caucvgprlemdisj  7734  caucvgprprlemdisj  7762  caucvgsr  7862  lelttr  8108  nnsub  9021  nn0ge2m1nn  9300  elnnz  9327  elnn0z  9330  indstr  9658  indstr2  9674  xrltnsym  9859  xrlttr  9861  xrltso  9862  xrlelttr  9872  xltnegi  9901  xsubge0  9947  ixxdisj  9969  icodisj  10058  fzm1  10166  qbtwnxr  10326  frec2uzlt2d  10475  nn0ltexp2  10780  facdiv  10809  resqrexlemgt0  11164  climuni  11436  fsumcl2lem  11541  dvdsle  11986  prmdvdsexpr  12288  prmfac1  12290  sqrt2irr  12300  phibndlem  12354  dvdsprmpweqle  12475  isxmet2d  14516  lgsdir2lem2  15145  lgseisenlem2  15187  trilpolemres  15532