Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( 𝜒 → 𝜒 ) |
2 |
1
|
olci |
⊢ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) |
3 |
1
|
olci |
⊢ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) |
4 |
2 3
|
pm3.2i |
⊢ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ) |
5 |
1
|
olci |
⊢ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) |
6 |
1
|
olci |
⊢ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) |
7 |
5 6
|
pm3.2i |
⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ) |
8 |
|
ifpim123g |
⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜒 ) → if- ( 𝜓 , 𝜒 , 𝜒 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ) ) ) |
9 |
4 7 8
|
mpbir2an |
⊢ ( if- ( 𝜑 , 𝜒 , 𝜒 ) → if- ( 𝜓 , 𝜒 , 𝜒 ) ) |
10 |
1
|
olci |
⊢ ( ( 𝜓 → ¬ 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) |
11 |
10 5
|
pm3.2i |
⊢ ( ( ( 𝜓 → ¬ 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ) |
12 |
1
|
olci |
⊢ ( ( ¬ 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) |
13 |
3 12
|
pm3.2i |
⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ) |
14 |
|
ifpim123g |
⊢ ( ( if- ( 𝜓 , 𝜒 , 𝜒 ) → if- ( 𝜑 , 𝜒 , 𝜒 ) ) ↔ ( ( ( ( 𝜓 → ¬ 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ) ) ) |
15 |
11 13 14
|
mpbir2an |
⊢ ( if- ( 𝜓 , 𝜒 , 𝜒 ) → if- ( 𝜑 , 𝜒 , 𝜒 ) ) |
16 |
9 15
|
impbii |
⊢ ( if- ( 𝜑 , 𝜒 , 𝜒 ) ↔ if- ( 𝜓 , 𝜒 , 𝜒 ) ) |