theorem an6lr (a b c d e f g h: wff):
$ a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> b $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
an5lr |
a /\ b /\ c /\ d /\ e /\ f /\ g -> b |
| 2 |
1 |
anwl |
a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> b |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)