Theorem pm2.21d 619

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

This theorem is referenced by:  pm2.21dd  620  pm5.21  695  2falsed  702  mtord  783  prlem1  973  eq0rdv  3469  csbprc  3470  rzal  3522  poirr2  5023  nnsucuniel  6498  nnawordex  6532  swoord2  6567  difinfsnlem  7100  exmidomni  7142  elni2  7315  cauappcvgprlemdisj  7652  caucvgprlemdisj  7675  caucvgprprlemdisj  7703  caucvgsr  7803  lelttr  8048  nnsub  8960  nn0ge2m1nn  9238  elnnz  9265  elnn0z  9268  indstr  9595  indstr2  9611  xrltnsym  9795  xrlttr  9797  xrltso  9798  xrlelttr  9808  xltnegi  9837  xsubge0  9883  ixxdisj  9905  icodisj  9994  fzm1  10102  qbtwnxr  10260  frec2uzlt2d  10406  nn0ltexp2  10691  facdiv  10720  resqrexlemgt0  11031  climuni  11303  fsumcl2lem  11408  dvdsle  11852  prmdvdsexpr  12152  prmfac1  12154  sqrt2irr  12164  phibndlem  12218  dvdsprmpweqle  12338  isxmet2d  13887  lgsdir2lem2  14469  lgseisenlem2  14490  trilpolemres  14829