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 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) | |
| Assertion | exbiriVD | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exbiriVD.1 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) | |
| 2 | idn3 | ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜃 ) | |
| 3 | idn2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) | |
| 4 | idn1 | ⊢ ( 𝜑 ▶ 𝜑 ) | |
| 5 | pm3.3 | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) → ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) ) ) | |
| 6 | 5 | com12 | ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) ) ) |
| 7 | 4 1 6 | e10 | ⊢ ( 𝜑 ▶ ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) ) |
| 8 | pm2.27 | ⊢ ( 𝜓 → ( ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) → ( 𝜒 ↔ 𝜃 ) ) ) | |
| 9 | 3 7 8 | e21 | ⊢ ( 𝜑 , 𝜓 ▶ ( 𝜒 ↔ 𝜃 ) ) |
| 10 | biimpr | ⊢ ( ( 𝜒 ↔ 𝜃 ) → ( 𝜃 → 𝜒 ) ) | |
| 11 | 10 | com12 | ⊢ ( 𝜃 → ( ( 𝜒 ↔ 𝜃 ) → 𝜒 ) ) |
| 12 | 2 9 11 | e32 | ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜒 ) |
| 13 | 12 | in3 | ⊢ ( 𝜑 , 𝜓 ▶ ( 𝜃 → 𝜒 ) ) |
| 14 | 13 | in2 | ⊢ ( 𝜑 ▶ ( 𝜓 → ( 𝜃 → 𝜒 ) ) ) |
| 15 | 14 | in1 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜒 ) ) ) |