Theorem a3d 78

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 79  pm2.21d 81  pm2.18 84  con2 94  con1 96  pm2.521 109  mt4d 121  ax4 1013  necon4ad 1673  necon4bd 1674  cla42gv 1912  cla43gv 1914  ra4esbca 2049  iununi 2671  limom 3203  isomin 3957  preleq 4665  sdomel 4912  cardsdomel 4917  ltapr 5216  suplem2pr 5227  lt2msqi 5941  qsqueeze 6333  om2uzlt2i 6557  infpnlem1 7598  infxpidmlem12 7655  atcv0eq 10390  iintlem1 10714

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

Copyright terms: Public domain