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  3553  csbprc  3554  rzal  3607  poirr2  5155  nnsucuniel  6728  nnawordex  6762  swoord2  6797  difinfsnlem  7390  exmidomni  7433  elni2  7629  cauappcvgprlemdisj  7966  caucvgprlemdisj  7989  caucvgprprlemdisj  8017  caucvgsr  8117  lelttr  8362  nnsub  9276  nn0ge2m1nn  9560  elnnz  9587  elnn0z  9590  indstr  9925  indstr2  9941  xrltnsym  10126  xrlttr  10128  xrltso  10129  xrlelttr  10139  xltnegi  10168  xsubge0  10214  ixxdisj  10236  icodisj  10325  fzm1  10434  qbtwnxr  10617  frec2uzlt2d  10766  nn0ltexp2  11071  facdiv  11100  resqrexlemgt0  11705  climuni  11978  fsumcl2lem  12084  dvdsle  12530  prmdvdsexpr  12847  prmfac1  12849  sqrt2irr  12859  phibndlem  12913  dvdsprmpweqle  13035  isxmet2d  15213  lgsdir2lem2  15902  lgseisenlem2  15944  wlkv0  16364  trilpolemres  16826