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  3482  csbprc  3483  rzal  3535  poirr2  5039  nnsucuniel  6521  nnawordex  6555  swoord2  6590  difinfsnlem  7129  exmidomni  7171  elni2  7344  cauappcvgprlemdisj  7681  caucvgprlemdisj  7704  caucvgprprlemdisj  7732  caucvgsr  7832  lelttr  8077  nnsub  8989  nn0ge2m1nn  9267  elnnz  9294  elnn0z  9297  indstr  9625  indstr2  9641  xrltnsym  9825  xrlttr  9827  xrltso  9828  xrlelttr  9838  xltnegi  9867  xsubge0  9913  ixxdisj  9935  icodisj  10024  fzm1  10132  qbtwnxr  10290  frec2uzlt2d  10437  nn0ltexp2  10724  facdiv  10753  resqrexlemgt0  11064  climuni  11336  fsumcl2lem  11441  dvdsle  11885  prmdvdsexpr  12185  prmfac1  12187  sqrt2irr  12197  phibndlem  12251  dvdsprmpweqle  12372  isxmet2d  14325  lgsdir2lem2  14908  lgseisenlem2  14929  trilpolemres  15269