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 972  necon4ad 1626  necon4bd 1627  cla42gv 1865  cla43gv 1867  ra4esbca 1999  iununi 2616  limom 3146  isomin 3899  preleq 4603  sdomel 4847  cardsdomel 4852  ltapr 5151  suplem2pr 5162  lt2msq 5881  qsqueeze 6280  om2uzlt2 6299  infpnlem1 7506  infxpidmlem12 7563  atcv0eq 10306  iintlem1 10632

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

Copyright terms: Public domain