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  703  2falsed  710  mtord  791  prlem1  982  eq0rdv  3555  csbprc  3556  rzal  3609  poirr2  5157  nnsucuniel  6730  nnawordex  6764  swoord2  6799  difinfsnlem  7392  exmidomni  7435  elni2  7631  cauappcvgprlemdisj  7968  caucvgprlemdisj  7991  caucvgprprlemdisj  8019  caucvgsr  8119  lelttr  8364  nnsub  9278  nn0ge2m1nn  9562  elnnz  9589  elnn0z  9592  indstr  9928  indstr2  9944  xrltnsym  10129  xrlttr  10131  xrltso  10132  xrlelttr  10142  xltnegi  10171  xsubge0  10217  ixxdisj  10239  icodisj  10328  fzm1  10438  qbtwnxr  10621  frec2uzlt2d  10770  nn0ltexp2  11075  facdiv  11104  resqrexlemgt0  11709  climuni  11982  fsumcl2lem  12088  dvdsle  12534  prmdvdsexpr  12851  prmfac1  12853  sqrt2irr  12863  phibndlem  12917  dvdsprmpweqle  13039  isxmet2d  15230  lgsdir2lem2  15919  lgseisenlem2  15961  wlkv0  16381  trilpolemres  16843