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 667  bianfd 740  a12stdy4 1377  sbc2or 1961  opth2 2806  findsg 3163  tfindsg 3168  funopg 3553  ensdomtr 4477  sdomen2 4488  suc11reg 4614  axunndlem1 4959  axunnd 4960  axpownd 4965  axregndlem1 4966  axregndlem2 4967  axinfndlem1 4969  axinfnd 4970  axacndlem1 4971  axacndlem2 4972  axacndlem3 4973  axacndlem4 4974  axacndlem5 4975  axacnd 4976  ltapr 5163  xrltnsymt 5562  xrlttrt 5565  add20 5614  prodgt0 5821  squeeze0 5926  nnleltp1t 5956  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxrre 6085  xrsup0 6099  elnnz 6147  qbtwnxr 6280  eliooret 6387  abssubne0t 6882  facdivt 6942  bccl2t 6971  climcl 6978  clmi1 7086  0top 7634  metxp 7831  tgioolem 7911  bcthlem18 8013  efif1lem7 8731

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

Copyright terms: Public domain