Metamath Proof Explorer

Theorem ovif12

Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Assertion ovif12 ${⊢}if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)=if\left({\phi },{A}{F}{C},{B}{F}{D}\right)$

Proof

Step Hyp Ref Expression
1 iftrue ${⊢}{\phi }\to if\left({\phi },{A},{B}\right)={A}$
2 iftrue ${⊢}{\phi }\to if\left({\phi },{C},{D}\right)={C}$
3 1 2 oveq12d ${⊢}{\phi }\to if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)={A}{F}{C}$
4 iftrue ${⊢}{\phi }\to if\left({\phi },{A}{F}{C},{B}{F}{D}\right)={A}{F}{C}$
5 3 4 eqtr4d ${⊢}{\phi }\to if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)=if\left({\phi },{A}{F}{C},{B}{F}{D}\right)$
6 iffalse ${⊢}¬{\phi }\to if\left({\phi },{A},{B}\right)={B}$
7 iffalse ${⊢}¬{\phi }\to if\left({\phi },{C},{D}\right)={D}$
8 6 7 oveq12d ${⊢}¬{\phi }\to if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)={B}{F}{D}$
9 iffalse ${⊢}¬{\phi }\to if\left({\phi },{A}{F}{C},{B}{F}{D}\right)={B}{F}{D}$
10 8 9 eqtr4d ${⊢}¬{\phi }\to if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)=if\left({\phi },{A}{F}{C},{B}{F}{D}\right)$
11 5 10 pm2.61i ${⊢}if\left({\phi },{A},{B}\right){F}if\left({\phi },{C},{D}\right)=if\left({\phi },{A}{F}{C},{B}{F}{D}\right)$