theorem piman {x: nat} (a b c: wff x):
$ (P. x a -> b) /\ (P. x a -> c) -> (P. x a -> b /\ c) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
anll |
E. x a /\ A. x (a -> b) /\ (P. x a -> c) -> E. x a |
| 2 |
1 |
conv pim |
(P. x a -> b) /\ (P. x a -> c) -> E. x a |
| 3 |
|
ralan |
A. x (a -> b /\ c) <-> A. x (a -> b) /\ A. x (a -> c) |
| 4 |
|
anim |
((P. x a -> b) -> A. x (a -> b)) -> ((P. x a -> c) -> A. x (a -> c)) -> (P. x a -> b) /\ (P. x a -> c) -> A. x (a -> b) /\ A. x (a -> c) |
| 5 |
|
anr |
E. x a /\ A. x (a -> b) -> A. x (a -> b) |
| 6 |
5 |
conv pim |
(P. x a -> b) -> A. x (a -> b) |
| 7 |
4, 6 |
ax_mp |
((P. x a -> c) -> A. x (a -> c)) -> (P. x a -> b) /\ (P. x a -> c) -> A. x (a -> b) /\ A. x (a -> c) |
| 8 |
|
anr |
E. x a /\ A. x (a -> c) -> A. x (a -> c) |
| 9 |
8 |
conv pim |
(P. x a -> c) -> A. x (a -> c) |
| 10 |
7, 9 |
ax_mp |
(P. x a -> b) /\ (P. x a -> c) -> A. x (a -> b) /\ A. x (a -> c) |
| 11 |
3, 10 |
sylibr |
(P. x a -> b) /\ (P. x a -> c) -> A. x (a -> b /\ c) |
| 12 |
2, 11 |
iand |
(P. x a -> b) /\ (P. x a -> c) -> E. x a /\ A. x (a -> b /\ c) |
| 13 |
12 |
conv pim |
(P. x a -> b) /\ (P. x a -> c) -> (P. x a -> b /\ c) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4)