Step |
Hyp |
Ref |
Expression |
1 |
|
dfifp2 |
⊢ ( if- ( 𝜑 , ( 𝜓 ∨ 𝜒 ) , ( 𝜃 ∨ 𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) ) |
2 |
|
df-or |
⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ( ¬ 𝜓 → 𝜒 ) ) |
3 |
2
|
imbi2i |
⊢ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ) |
4 |
|
df-or |
⊢ ( ( 𝜃 ∨ 𝜏 ) ↔ ( ¬ 𝜃 → 𝜏 ) ) |
5 |
4
|
imbi2i |
⊢ ( ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ↔ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) |
6 |
3 5
|
anbi12i |
⊢ ( ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) ) |
7 |
|
ifpimimb |
⊢ ( if- ( 𝜑 , ( ¬ 𝜓 → 𝜒 ) , ( ¬ 𝜃 → 𝜏 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
8 |
|
dfifp2 |
⊢ ( if- ( 𝜑 , ( ¬ 𝜓 → 𝜒 ) , ( ¬ 𝜃 → 𝜏 ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) ) |
9 |
|
imor |
⊢ ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
10 |
|
ifpnot23d |
⊢ ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ↔ if- ( 𝜑 , 𝜓 , 𝜃 ) ) |
11 |
10
|
orbi1i |
⊢ ( ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
12 |
9 11
|
bitri |
⊢ ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
13 |
7 8 12
|
3bitr3i |
⊢ ( ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
14 |
1 6 13
|
3bitri |
⊢ ( if- ( 𝜑 , ( 𝜓 ∨ 𝜒 ) , ( 𝜃 ∨ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |