Theorem pm2.21d 549

Description: A contradiction implies anything. Deduction from pm2.21 547. (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 547	. 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 545

This theorem is referenced by:  pm2.21dd  550  pm5.21  611  2falsed  618  mtord  697  prlem1  880  eq0rdv  3261  csbprc  3262  rzal  3318  poirr2  4717  nnawordex  6101  swoord2  6136  elni2  6412  cauappcvgprlemdisj  6749  caucvgprlemdisj  6772  caucvgprprlemdisj  6800  caucvgsr  6886  lelttr  7106  nnsub  7952  nn0ge2m1nn  8242  elnnz  8255  elnn0z  8258  indstr  8536  indstr2  8546  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlelttr  8722  xltnegi  8748  ixxdisj  8772  icodisj  8860  fzm1  8962  frec2uzlt2d  9190  expival  9257  resqrexlemgt0  9618  climuni  9814  sqrt2irr  9878