Step |
Hyp |
Ref |
Expression |
1 |
|
iftrue |
⊢ ( ( 𝜑 ∨ 𝜓 ) → if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) = 𝐴 ) |
2 |
1
|
orcs |
⊢ ( 𝜑 → if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) = 𝐴 ) |
3 |
|
iftrue |
⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐴 , 𝐵 ) ) = 𝐴 ) |
4 |
2 3
|
eqtr4d |
⊢ ( 𝜑 → if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐴 , 𝐵 ) ) ) |
5 |
|
iffalse |
⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐴 , 𝐵 ) ) = if ( 𝜓 , 𝐴 , 𝐵 ) ) |
6 |
|
biorf |
⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) ) |
7 |
6
|
ifbid |
⊢ ( ¬ 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) ) |
8 |
5 7
|
eqtr2d |
⊢ ( ¬ 𝜑 → if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐴 , 𝐵 ) ) ) |
9 |
4 8
|
pm2.61i |
⊢ if ( ( 𝜑 ∨ 𝜓 ) , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐴 , 𝐵 ) ) |