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 663  bianfd 736  a12stdy4 1368  sbc2or 1948  opth2 2789  findsg 3147  tfindsg 3152  funopg 3533  ensdomtr 4451  sdomen2 4462  suc11reg 4577  axunndlem1 4919  axunnd 4920  axpownd 4925  axregndlem1 4926  axregndlem2 4927  axinfndlem1 4929  axinfnd 4930  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacndlem5 4935  axacnd 4936  ltapr 5123  xrltnsymt 5523  xrlttrt 5526  add20 5576  prodgt0 5775  squeeze0 5872  nnleltp1t 5901  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  xrsup0 6044  elnnz 6092  qbtwnxr 6217  abssubne0t 6820  facdivt 6879  bccl2t 6909  climcl 6916  clmi1 7024  0top 7577  metxp 7774  tgioolem 7853  bcthlem18 7950  efif1lem7 8651

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

Copyright terms: Public domain