Theorem pm2.21d 78

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

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 12	. 2 |- (ph -> (-. ch -> -. ps))
3	2	a3d 75	1 |- (ph -> (ps -> ch))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.5 100  pm5.14 665  bianfd 738  a12stdy4 1375  sbc2or 1958  opth2 2800  findsg 3157  tfindsg 3162  funopg 3547  ensdomtr 4471  sdomen2 4482  suc11reg 4605  axunndlem1 4947  axunnd 4948  axpownd 4953  axregndlem1 4954  axregndlem2 4955  axinfndlem1 4957  axinfnd 4958  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacndlem5 4963  axacnd 4964  ltapr 5151  xrltnsymt 5550  xrlttrt 5553  add20 5602  prodgt0 5819  squeeze0 5924  nnleltp1t 5954  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrre 6083  xrsup0 6097  elnnz 6145  qbtwnxr 6279  eliooret 6386  abssubne0t 6882  facdivt 6942  bccl2t 6971  climcl 6978  clmi1 7086  0top 7635  metxp 7834  tgioolem 7914  bcthlem18 8016  efif1lem7 8736

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

Copyright terms: Public domain