Theorem a3d 70

Description: Deduction derived from axiom ax-3 5.

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 5	. 2 |- ((-. ps -> -. ch) -> (ch -> ps))
3	1, 2	syl 12	1 |- (ph -> (ch -> ps))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  pm2.21 71  pm2.21d 74  pm2.18 75  con2 82  con1 84  cla42gv 1399  iununi 2037  limom 2387  isomin 2937  oa00 3161  preleq 3454  zfregs 3491  aceq5 3563  sdomel 3653  cardsdomel 3658  ltapr 3945  suplem2pr 3956  lt2sq 4414  nn0opth 4724  infxpidmlem12 4944  his6 5057  atcv0eq 5767

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

metamath.org