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  5120  nnsucuniel  6639  nnawordex  6673  swoord2  6708  difinfsnlem  7262  exmidomni  7305  elni2  7497  cauappcvgprlemdisj  7834  caucvgprlemdisj  7857  caucvgprprlemdisj  7885  caucvgsr  7985  lelttr  8231  nnsub  9145  nn0ge2m1nn  9425  elnnz  9452  elnn0z  9455  indstr  9784  indstr2  9800  xrltnsym  9985  xrlttr  9987  xrltso  9988  xrlelttr  9998  xltnegi  10027  xsubge0  10073  ixxdisj  10095  icodisj  10184  fzm1  10292  qbtwnxr  10472  frec2uzlt2d  10621  nn0ltexp2  10926  facdiv  10955  resqrexlemgt0  11526  climuni  11799  fsumcl2lem  11904  dvdsle  12350  prmdvdsexpr  12667  prmfac1  12669  sqrt2irr  12679  phibndlem  12733  dvdsprmpweqle  12855  isxmet2d  15016  lgsdir2lem2  15702  lgseisenlem2  15744  trilpolemres  16369