Theorem pm2.21d 624

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

This theorem is referenced by:  pm2.21dd  625  pm5.21  702  2falsed  709  mtord  790  prlem1  981  eq0rdv  3539  csbprc  3540  rzal  3592  poirr2  5129  nnsucuniel  6662  nnawordex  6696  swoord2  6731  difinfsnlem  7297  exmidomni  7340  elni2  7533  cauappcvgprlemdisj  7870  caucvgprlemdisj  7893  caucvgprprlemdisj  7921  caucvgsr  8021  lelttr  8267  nnsub  9181  nn0ge2m1nn  9461  elnnz  9488  elnn0z  9491  indstr  9826  indstr2  9842  xrltnsym  10027  xrlttr  10029  xrltso  10030  xrlelttr  10040  xltnegi  10069  xsubge0  10115  ixxdisj  10137  icodisj  10226  fzm1  10334  qbtwnxr  10516  frec2uzlt2d  10665  nn0ltexp2  10970  facdiv  10999  resqrexlemgt0  11580  climuni  11853  fsumcl2lem  11958  dvdsle  12404  prmdvdsexpr  12721  prmfac1  12723  sqrt2irr  12733  phibndlem  12787  dvdsprmpweqle  12909  isxmet2d  15071  lgsdir2lem2  15757  lgseisenlem2  15799  wlkv0  16219  trilpolemres  16646