Description: Virtual deduction proof of exbiri . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
| h1:: | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
| 2:: | |- (. ph ->. ph ). |
| 3:: | |- (. ph ,. ps ->. ps ). |
| 4:: | |- (. ph ,. ps ,. th ->. th ). |
| 5:2,1,?: e10 | |- (. ph ->. ( ps -> ( ch <-> th ) ) ). |
| 6:3,5,?: e21 | |- (. ph ,. ps ->. ( ch <-> th ) ). |
| 7:4,6,?: e32 | |- (. ph ,. ps ,. th ->. ch ). |
| 8:7: | |- (. ph ,. ps ->. ( th -> ch ) ). |
| 9:8: | |- (. ph ->. ( ps -> ( th -> ch ) ) ). |
| qed:9: | |- ( ph -> ( ps -> ( th -> ch ) ) ) |
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | exbiriVD.1 | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
|
| Assertion | exbiriVD | |- ( ph -> ( ps -> ( th -> ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exbiriVD.1 | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
|
| 2 | idn3 | |- (. ph ,. ps ,. th ->. th ). |
|
| 3 | idn2 | |- (. ph ,. ps ->. ps ). |
|
| 4 | idn1 | |- (. ph ->. ph ). |
|
| 5 | pm3.3 | |- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( ch <-> th ) ) ) ) |
|
| 6 | 5 | com12 | |- ( ph -> ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ps -> ( ch <-> th ) ) ) ) |
| 7 | 4 1 6 | e10 | |- (. ph ->. ( ps -> ( ch <-> th ) ) ). |
| 8 | pm2.27 | |- ( ps -> ( ( ps -> ( ch <-> th ) ) -> ( ch <-> th ) ) ) |
|
| 9 | 3 7 8 | e21 | |- (. ph ,. ps ->. ( ch <-> th ) ). |
| 10 | biimpr | |- ( ( ch <-> th ) -> ( th -> ch ) ) |
|
| 11 | 10 | com12 | |- ( th -> ( ( ch <-> th ) -> ch ) ) |
| 12 | 2 9 11 | e32 | |- (. ph ,. ps ,. th ->. ch ). |
| 13 | 12 | in3 | |- (. ph ,. ps ->. ( th -> ch ) ). |
| 14 | 13 | in2 | |- (. ph ->. ( ps -> ( th -> ch ) ) ). |
| 15 | 14 | in1 | |- ( ph -> ( ps -> ( th -> ch ) ) ) |