Theorem pm2.21d 74

Description: A contradiction implies anything. Deduction from pm2.21 71.

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	. . 3 |- (ph -> -. ps)
2	1	a1d 14	. 2 |- (ph -> (-. ch -> -. ps))
3	2	a3d 70	1 |- (ph -> (ps -> ch))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  nbn 542  bianfd 554  sbc2or 1454  opth2 1909  findsg 2398  tfindsg 2402  abianfp 3000  ensdomtr 3372  sdomen2 3380  suc11reg 3456  axunndlem1 3741  axunnd 3742  axpownd 3747  axregndlem1 3748  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacndlem5 3757  axacnd 3758  ltapr 3945  add20 4329  nnleltp1t 4448  elnnz 4572

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org