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 ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is referenced by:  pm2.21dd  629  pm5.21  707  2falsed  714  mtord  795  prlem1  986  eq0rdv  3570  csbprc  3571  rzal  3622  ifeqeqxdc  3684  poirr2  5175  nnsucuniel  6758  nnawordex  6792  swoord2  6827  difinfsnlem  7429  exmidomni  7472  elni2  7671  cauappcvgprlemdisj  8008  caucvgprlemdisj  8031  caucvgprprlemdisj  8059  caucvgsr  8159  lelttr  8404  nnsub  9322  nn0ge2m1nn  9606  elnnz  9633  elnn0z  9636  indstr  9972  indstr2  9988  xrltnsym  10174  xrlttr  10176  xrltso  10177  xrlelttr  10187  xltnegi  10216  xsubge0  10262  ixxdisj  10284  icodisj  10373  fzm1  10485  qbtwnxr  10670  frec2uzlt2d  10819  nn0ltexp2  11125  facdiv  11154  resqrexlemgt0  11764  climuni  12037  fsumcl2lem  12143  dvdsle  12589  prmdvdsexpr  12906  prmfac1  12908  sqrt2irr  12918  phibndlem  12972  dvdsprmpweqle  13094  isxmet2d  15372  lgsdir2lem2  16062  lgseisenlem2  16104  wlkv0  16524  trilpolemres  16996