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  necon4ad 1602  necon4bd 1603  cla42gv 1840  ra4esbca 1970  iununi 2584  limom 3109  isomin 3838  preleq 4527  sdomel 4770  cardsdomel 4775  ltapr 5074  suplem2pr 5085  lt2msq 5780  qsqueeze 6169  om2uzlt2 6187  nn0opth 6547  infpnlem1 7400  infxpidmlem12 7457  iintlem1 8826  atcv0eq 10428

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

Copyright terms: Public domain