Theorem pm2.21d 608

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

This theorem is referenced by:  pm2.21dd  609  pm5.21  684  2falsed  691  mtord  772  prlem1  957  eq0rdv  3402  csbprc  3403  rzal  3455  poirr2  4926  nnsucuniel  6384  nnawordex  6417  swoord2  6452  difinfsnlem  6977  exmidomni  7007  elni2  7115  cauappcvgprlemdisj  7452  caucvgprlemdisj  7475  caucvgprprlemdisj  7503  caucvgsr  7603  lelttr  7845  nnsub  8752  nn0ge2m1nn  9030  elnnz  9057  elnn0z  9060  indstr  9381  indstr2  9396  xrltnsym  9572  xrlttr  9574  xrltso  9575  xrlelttr  9582  xltnegi  9611  xsubge0  9657  ixxdisj  9679  icodisj  9768  fzm1  9873  qbtwnxr  10028  frec2uzlt2d  10170  facdiv  10477  resqrexlemgt0  10785  climuni  11055  fsumcl2lem  11160  dvdsle  11531  prmdvdsexpr  11817  prmfac1  11819  sqrt2irr  11829  phibndlem  11881  isxmet2d  12506  trilpolemres  13224