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  5183  nnsucuniel  6773  nnawordex  6807  swoord2  6842  difinfsnlem  7445  exmidomni  7488  elni2  7687  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  caucvgsr  8175  lelttr  8420  nnsub  9352  nn0ge2m1nn  9636  elnnz  9663  elnn0z  9666  indstr  10008  indstr2  10024  xrltnsym  10211  xrlttr  10213  xrltso  10214  xrlelttr  10224  xltnegi  10253  xsubge0  10299  ixxdisj  10321  icodisj  10410  fzm1  10523  qbtwnxr  10708  frec2uzlt2d  10861  nn0ltexp2  11168  facdiv  11197  resqrexlemgt0  11807  climuni  12083  fsumcl2lem  12189  dvdsle  12635  prmdvdsexpr  12953  prmfac1  12955  sqrt2irr  12965  phibndlem  13022  dvdsprmpweqle  13144  prmlem1  13250  prmlem2  13262  isxmet2d  15591  bpos1  16327  lgsdir2lem2  16370  lgseisenlem2  16412  wlkv0  16832  trilpolemres  17315