Theorem pm2.21d 549

Description: A contradiction implies anything. Deduction from pm2.21 547. (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 547	. 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-1 5  ax-2 6  ax-mp 7  ax-in2 545

This theorem is referenced by:  pm2.21dd  550  pm5.21  610  2falsed  617  mtord  696  prlem1  879  eq0rdv  3255  csbprc  3256  rzal  3312  poirr2  4660  nnawordex  6037  swoord2  6072  elni2  6298  cauappcvgprlemdisj  6623  caucvgprlemdisj  6645  lelttr  6903  nnsub  7733  nn0ge2m1nn  8018  elnnz  8031  elnn0z  8034  indstr  8312  indstr2  8322  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlelttr  8492  xltnegi  8518  ixxdisj  8542  icodisj  8630  fzm1  8732  frec2uzlt2d  8871  expival  8911