Theorem pm2.21d 622

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

This theorem is referenced by:  pm2.21dd  623  pm5.21  700  2falsed  707  mtord  788  prlem1  979  eq0rdv  3536  csbprc  3537  rzal  3589  poirr2  5121  nnsucuniel  6649  nnawordex  6683  swoord2  6718  difinfsnlem  7277  exmidomni  7320  elni2  7512  cauappcvgprlemdisj  7849  caucvgprlemdisj  7872  caucvgprprlemdisj  7900  caucvgsr  8000  lelttr  8246  nnsub  9160  nn0ge2m1nn  9440  elnnz  9467  elnn0z  9470  indstr  9800  indstr2  9816  xrltnsym  10001  xrlttr  10003  xrltso  10004  xrlelttr  10014  xltnegi  10043  xsubge0  10089  ixxdisj  10111  icodisj  10200  fzm1  10308  qbtwnxr  10489  frec2uzlt2d  10638  nn0ltexp2  10943  facdiv  10972  resqrexlemgt0  11546  climuni  11819  fsumcl2lem  11924  dvdsle  12370  prmdvdsexpr  12687  prmfac1  12689  sqrt2irr  12699  phibndlem  12753  dvdsprmpweqle  12875  isxmet2d  15037  lgsdir2lem2  15723  lgseisenlem2  15765  wlkv0  16110  trilpolemres  16470