Theorem pm2.21d 620

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

This theorem is referenced by:  pm2.21dd  621  pm5.21  696  2falsed  703  mtord  784  prlem1  975  eq0rdv  3504  csbprc  3505  rzal  3557  poirr2  5074  nnsucuniel  6580  nnawordex  6614  swoord2  6649  difinfsnlem  7200  exmidomni  7243  elni2  7426  cauappcvgprlemdisj  7763  caucvgprlemdisj  7786  caucvgprprlemdisj  7814  caucvgsr  7914  lelttr  8160  nnsub  9074  nn0ge2m1nn  9354  elnnz  9381  elnn0z  9384  indstr  9713  indstr2  9729  xrltnsym  9914  xrlttr  9916  xrltso  9917  xrlelttr  9927  xltnegi  9956  xsubge0  10002  ixxdisj  10024  icodisj  10113  fzm1  10221  qbtwnxr  10398  frec2uzlt2d  10547  nn0ltexp2  10852  facdiv  10881  resqrexlemgt0  11273  climuni  11546  fsumcl2lem  11651  dvdsle  12097  prmdvdsexpr  12414  prmfac1  12416  sqrt2irr  12426  phibndlem  12480  dvdsprmpweqle  12602  isxmet2d  14762  lgsdir2lem2  15448  lgseisenlem2  15490  trilpolemres  15914