Description: Implication form of imbi12i . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 is imbi12VD without virtual deductions and was automatically derived from imbi12VD .
1:: | |- (. ( ph <-> ps ) ->. ( ph <-> ps ) ). |
2:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ->. ( ch <-> th ) ). |
3:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph -> ch ) ->. ( ph -> ch ) ). |
4:1,3: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph -> ch ) ->. ( ps -> ch ) ). |
5:2,4: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ph -> ch ) ->. ( ps -> th ) ). |
6:5: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ->. ( ( ph -> ch ) -> ( ps -> th ) ) ). |
7:: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps -> th ) ->. ( ps -> th ) ). |
8:1,7: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps -> th ) ->. ( ph -> th ) ). |
9:2,8: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ,. ( ps -> th ) ->. ( ph -> ch ) ). |
10:9: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ->. ( ( ps -> th ) -> ( ph -> ch ) ) ). |
11:6,10: | |- (. ( ph <-> ps ) ,. ( ch <-> th ) ->. ( ( ph -> ch ) <-> ( ps -> th ) ) ). |
12:11: | |- (. ( ph <-> ps ) ->. ( ( ch <-> th ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) ) ). |
qed:12: | |- ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) ) ) |
Ref | Expression | ||
---|---|---|---|
Assertion | imbi12VD | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) ▶ ( 𝜒 ↔ 𝜃 ) ) | |
2 | idn1 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ▶ ( 𝜑 ↔ 𝜓 ) ) | |
3 | idn3 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜑 → 𝜒 ) ▶ ( 𝜑 → 𝜒 ) ) | |
4 | biimpr | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜓 → 𝜑 ) ) | |
5 | 4 | imim1d | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 → 𝜒 ) → ( 𝜓 → 𝜒 ) ) ) |
6 | 2 3 5 | e13 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜑 → 𝜒 ) ▶ ( 𝜓 → 𝜒 ) ) |
7 | biimp | ⊢ ( ( 𝜒 ↔ 𝜃 ) → ( 𝜒 → 𝜃 ) ) | |
8 | 7 | imim2d | ⊢ ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜓 → 𝜒 ) → ( 𝜓 → 𝜃 ) ) ) |
9 | 1 6 8 | e23 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜑 → 𝜒 ) ▶ ( 𝜓 → 𝜃 ) ) |
10 | 9 | in3 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) ▶ ( ( 𝜑 → 𝜒 ) → ( 𝜓 → 𝜃 ) ) ) |
11 | idn3 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜓 → 𝜃 ) ▶ ( 𝜓 → 𝜃 ) ) | |
12 | biimp | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) ) | |
13 | 12 | imim1d | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜓 → 𝜃 ) → ( 𝜑 → 𝜃 ) ) ) |
14 | 2 11 13 | e13 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜓 → 𝜃 ) ▶ ( 𝜑 → 𝜃 ) ) |
15 | biimpr | ⊢ ( ( 𝜒 ↔ 𝜃 ) → ( 𝜃 → 𝜒 ) ) | |
16 | 15 | imim2d | ⊢ ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜒 ) ) ) |
17 | 1 14 16 | e23 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) , ( 𝜓 → 𝜃 ) ▶ ( 𝜑 → 𝜒 ) ) |
18 | 17 | in3 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) ▶ ( ( 𝜓 → 𝜃 ) → ( 𝜑 → 𝜒 ) ) ) |
19 | impbi | ⊢ ( ( ( 𝜑 → 𝜒 ) → ( 𝜓 → 𝜃 ) ) → ( ( ( 𝜓 → 𝜃 ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) ) | |
20 | 10 18 19 | e22 | ⊢ ( ( 𝜑 ↔ 𝜓 ) , ( 𝜒 ↔ 𝜃 ) ▶ ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) |
21 | 20 | in2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ▶ ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) ) |
22 | 21 | in1 | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) ) |