Theorem pm2.21d 584

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

This theorem is referenced by:  pm2.21dd  585  pm5.21  646  2falsed  653  mtord  732  prlem1  919  eq0rdv  3324  csbprc  3325  rzal  3375  poirr2  4811  nnsucuniel  6238  nnawordex  6267  swoord2  6302  exmidomni  6777  elni2  6852  cauappcvgprlemdisj  7189  caucvgprlemdisj  7212  caucvgprprlemdisj  7240  caucvgsr  7326  lelttr  7552  nnsub  8432  nn0ge2m1nn  8703  elnnz  8730  elnn0z  8733  indstr  9050  indstr2  9065  xrltnsym  9232  xrlttr  9234  xrltso  9235  xrlelttr  9240  xltnegi  9266  ixxdisj  9290  icodisj  9378  fzm1  9481  qbtwnxr  9634  frec2uzlt2d  9776  facdiv  10111  resqrexlemgt0  10418  climuni  10645  fsumcl2lem  10755  dvdsle  10927  prmdvdsexpr  11211  prmfac1  11213  sqrt2irr  11223  phibndlem  11274