Theorem pm2.21d 628

Description: A contradiction implies anything. Deduction from pm2.21 626. (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 626	. 2 |- ( -. ps -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21dd  629  pm5.21  707  2falsed  714  mtord  795  prlem1  986  eq0rdv  3571  csbprc  3572  rzal  3625  ifeqeqxdc  3687  poirr2  5180  nnsucuniel  6768  nnawordex  6802  swoord2  6837  difinfsnlem  7439  exmidomni  7482  elni2  7681  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  caucvgsr  8169  lelttr  8414  nnsub  9343  nn0ge2m1nn  9627  elnnz  9654  elnn0z  9657  indstr  9993  indstr2  10009  xrltnsym  10195  xrlttr  10197  xrltso  10198  xrlelttr  10208  xltnegi  10237  xsubge0  10283  ixxdisj  10305  icodisj  10394  fzm1  10507  qbtwnxr  10692  frec2uzlt2d  10841  nn0ltexp2  11147  facdiv  11176  resqrexlemgt0  11786  climuni  12059  fsumcl2lem  12165  dvdsle  12611  prmdvdsexpr  12928  prmfac1  12930  sqrt2irr  12940  phibndlem  12994  dvdsprmpweqle  13116  isxmet2d  15449  lgsdir2lem2  16148  lgseisenlem2  16190  wlkv0  16610  trilpolemres  17091