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  963  eq0rdv  3452  csbprc  3453  rzal  3505  poirr2  4995  nnsucuniel  6459  nnawordex  6492  swoord2  6527  difinfsnlem  7060  exmidomni  7102  elni2  7251  cauappcvgprlemdisj  7588  caucvgprlemdisj  7611  caucvgprprlemdisj  7639  caucvgsr  7739  lelttr  7983  nnsub  8892  nn0ge2m1nn  9170  elnnz  9197  elnn0z  9200  indstr  9527  indstr2  9543  xrltnsym  9725  xrlttr  9727  xrltso  9728  xrlelttr  9738  xltnegi  9767  xsubge0  9813  ixxdisj  9835  icodisj  9924  fzm1  10031  qbtwnxr  10189  frec2uzlt2d  10335  nn0ltexp2  10619  facdiv  10647  resqrexlemgt0  10958  climuni  11230  fsumcl2lem  11335  dvdsle  11778  prmdvdsexpr  12078  prmfac1  12080  sqrt2irr  12090  phibndlem  12144  dvdsprmpweqle  12264  isxmet2d  12948  lgsdir2lem2  13530  trilpolemres  13881