Theorem pm2.21d 581

Description: A contradiction implies anything. Deduction from pm2.21 579. (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 579	. 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-1 5  ax-2 6  ax-mp 7  ax-in2 577

This theorem is referenced by:  pm2.21dd  582  pm5.21  643  2falsed  650  mtord  729  prlem1  914  eq0rdv  3288  csbprc  3289  rzal  3338  poirr2  4737  nnawordex  6124  swoord2  6159  elni2  6504  cauappcvgprlemdisj  6841  caucvgprlemdisj  6864  caucvgprprlemdisj  6892  caucvgsr  6978  lelttr  7199  nnsub  8077  nn0ge2m1nn  8348  elnnz  8361  elnn0z  8364  indstr  8681  indstr2  8696  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlelttr  8876  xltnegi  8902  ixxdisj  8926  icodisj  9014  fzm1  9117  qbtwnxr  9266  frec2uzlt2d  9406  expival  9478  facdiv  9665  resqrexlemgt0  9906  climuni  10132  dvdsle  10244  prmdvdsexpr  10529  prmfac1  10531  sqrt2irr  10541