Theorem a3d 75

Description: Deduction derived from axiom ax-3 6.

Hypothesis

Ref	Expression
a3d.1	|- (ph -> (-. ps -> -. ch))

Assertion

Ref	Expression
a3d	|- (ph -> (ch -> ps))

Proof of Theorem a3d

Step	Hyp	Ref	Expression
1		a3d.1	. 2 |- (ph -> (-. ps -> -. ch))
2		ax-3 6	. 2 |- ((-. ps -> -. ch) -> (ch -> ps))
3	1, 2	syl 10	1 |- (ph -> (ch -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.21 76  pm2.21d 78  pm2.18 81  con2 90  con1 92  pm2.521 103  mt4d 115  ax4 974  necon4ad 1629  necon4bd 1630  cla42gv 1868  cla43gv 1870  ra4esbca 2003  iununi 2622  limom 3153  isomin 3906  preleq 4619  sdomel 4865  cardsdomel 4870  ltapr 5170  suplem2pr 5181  lt2msq 5890  qsqueeze 6288  om2uzlt2 6307  infpnlem1 7514  infxpidmlem12 7571  atcv0eq 10309  iintlem1 10611

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

Copyright terms: Public domain