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  9345  nn0ge2m1nn  9631  elnnz  9658  elnn0z  9661  indstr  10002  indstr2  10018  xrltnsym  10205  xrlttr  10207  xrltso  10208  xrlelttr  10218  xltnegi  10247  xsubge0  10293  ixxdisj  10315  icodisj  10404  fzm1  10517  qbtwnxr  10702  frec2uzlt2d  10854  nn0ltexp2  11161  facdiv  11190  resqrexlemgt0  11800  climuni  12075  fsumcl2lem  12181  dvdsle  12627  prmdvdsexpr  12945  prmfac1  12947  sqrt2irr  12957  phibndlem  13014  dvdsprmpweqle  13136  prmlem1  13242  prmlem2  13254  isxmet2d  15498  bpos1  16208  lgsdir2lem2  16246  lgseisenlem2  16288  wlkv0  16708  trilpolemres  17189