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  697  2falsed  704  mtord  785  prlem1  976  eq0rdv  3509  csbprc  3510  rzal  3562  poirr2  5084  nnsucuniel  6594  nnawordex  6628  swoord2  6663  difinfsnlem  7216  exmidomni  7259  elni2  7447  cauappcvgprlemdisj  7784  caucvgprlemdisj  7807  caucvgprprlemdisj  7835  caucvgsr  7935  lelttr  8181  nnsub  9095  nn0ge2m1nn  9375  elnnz  9402  elnn0z  9405  indstr  9734  indstr2  9750  xrltnsym  9935  xrlttr  9937  xrltso  9938  xrlelttr  9948  xltnegi  9977  xsubge0  10023  ixxdisj  10045  icodisj  10134  fzm1  10242  qbtwnxr  10422  frec2uzlt2d  10571  nn0ltexp2  10876  facdiv  10905  resqrexlemgt0  11406  climuni  11679  fsumcl2lem  11784  dvdsle  12230  prmdvdsexpr  12547  prmfac1  12549  sqrt2irr  12559  phibndlem  12613  dvdsprmpweqle  12735  isxmet2d  14895  lgsdir2lem2  15581  lgseisenlem2  15623  trilpolemres  16122