Theorem pm2.21d 609

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

This theorem is referenced by:  pm2.21dd  610  pm5.21  685  2falsed  692  mtord  773  prlem1  958  eq0rdv  3434  csbprc  3435  rzal  3487  poirr2  4971  nnsucuniel  6431  nnawordex  6464  swoord2  6499  difinfsnlem  7029  exmidomni  7064  elni2  7213  cauappcvgprlemdisj  7550  caucvgprlemdisj  7573  caucvgprprlemdisj  7601  caucvgsr  7701  lelttr  7944  nnsub  8851  nn0ge2m1nn  9129  elnnz  9156  elnn0z  9159  indstr  9483  indstr2  9498  xrltnsym  9678  xrlttr  9680  xrltso  9681  xrlelttr  9688  xltnegi  9717  xsubge0  9763  ixxdisj  9785  icodisj  9874  fzm1  9980  qbtwnxr  10135  frec2uzlt2d  10281  facdiv  10589  resqrexlemgt0  10897  climuni  11167  fsumcl2lem  11272  dvdsle  11709  prmdvdsexpr  11996  prmfac1  11998  sqrt2irr  12008  phibndlem  12060  isxmet2d  12695  trilpolemres  13562