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  5183  nnsucuniel  6772  nnawordex  6806  swoord2  6841  difinfsnlem  7445  exmidomni  7488  elni2  7687  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  caucvgsr  8175  lelttr  8420  nnsub  9352  nn0ge2m1nn  9638  elnnz  9665  elnn0z  9668  indstr  10009  indstr2  10025  xrltnsym  10212  xrlttr  10214  xrltso  10215  xrlelttr  10225  xltnegi  10254  xsubge0  10300  ixxdisj  10322  icodisj  10411  fzm1  10524  qbtwnxr  10709  frec2uzlt2d  10862  nn0ltexp2  11169  facdiv  11198  resqrexlemgt0  11808  climuni  12084  fsumcl2lem  12190  dvdsle  12636  prmdvdsexpr  12954  prmfac1  12956  sqrt2irr  12966  phibndlem  13023  dvdsprmpweqle  13145  prmlem1  13251  prmlem2  13263  isxmet2d  15574  bpos1  16310  lgsdir2lem2  16353  lgseisenlem2  16395  wlkv0  16815  trilpolemres  17298