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 969  necon4ad 1618  necon4bd 1619  cla42gv 1856  cla43gv 1858  ra4esbca 1989  iununi 2606  limom 3136  isomin 3884  preleq 4575  sdomel 4819  cardsdomel 4824  ltapr 5123  suplem2pr 5134  lt2msq 5829  qsqueeze 6218  om2uzlt2 6236  nn0opth 6596  infpnlem1 7449  infxpidmlem12 7506  atcv0eq 10214  iintlem1 10476

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

Copyright terms: Public domain