Theorem pm2.21d 628

Description: A contradiction implies anything. Deduction from pm2.21 626. (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 626	. 2 |- ( -. ps -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21dd  629  pm5.21  707  2falsed  714  mtord  795  prlem1  986  eq0rdv  3571  csbprc  3572  rzal  3625  ifeqeqxdc  3687  poirr2  5180  nnsucuniel  6768  nnawordex  6802  swoord2  6837  difinfsnlem  7440  exmidomni  7483  elni2  7682  cauappcvgprlemdisj  8019  caucvgprlemdisj  8042  caucvgprprlemdisj  8070  caucvgsr  8170  lelttr  8415  nnsub  9346  nn0ge2m1nn  9632  elnnz  9659  elnn0z  9662  indstr  10003  indstr2  10019  xrltnsym  10206  xrlttr  10208  xrltso  10209  xrlelttr  10219  xltnegi  10248  xsubge0  10294  ixxdisj  10316  icodisj  10405  fzm1  10518  qbtwnxr  10703  frec2uzlt2d  10856  nn0ltexp2  11163  facdiv  11192  resqrexlemgt0  11802  climuni  12078  fsumcl2lem  12184  dvdsle  12630  prmdvdsexpr  12948  prmfac1  12950  sqrt2irr  12960  phibndlem  13017  dvdsprmpweqle  13139  prmlem1  13245  prmlem2  13257  isxmet2d  15540  bpos1  16271  lgsdir2lem2  16314  lgseisenlem2  16356  wlkv0  16776  trilpolemres  17258