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  702  2falsed  709  mtord  790  prlem1  981  eq0rdv  3539  csbprc  3540  rzal  3592  poirr2  5129  nnsucuniel  6663  nnawordex  6697  swoord2  6732  difinfsnlem  7298  exmidomni  7341  elni2  7534  cauappcvgprlemdisj  7871  caucvgprlemdisj  7894  caucvgprprlemdisj  7922  caucvgsr  8022  lelttr  8268  nnsub  9182  nn0ge2m1nn  9462  elnnz  9489  elnn0z  9492  indstr  9827  indstr2  9843  xrltnsym  10028  xrlttr  10030  xrltso  10031  xrlelttr  10041  xltnegi  10070  xsubge0  10116  ixxdisj  10138  icodisj  10227  fzm1  10335  qbtwnxr  10518  frec2uzlt2d  10667  nn0ltexp2  10972  facdiv  11001  resqrexlemgt0  11598  climuni  11871  fsumcl2lem  11977  dvdsle  12423  prmdvdsexpr  12740  prmfac1  12742  sqrt2irr  12752  phibndlem  12806  dvdsprmpweqle  12928  isxmet2d  15091  lgsdir2lem2  15777  lgseisenlem2  15819  wlkv0  16239  trilpolemres  16697