MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovif Structured version   Visualization version   GIF version

Theorem ovif 6702
Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Assertion
Ref Expression
ovif (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶))

Proof of Theorem ovif
StepHypRef Expression
1 oveq1 6622 . 2 (if(𝜑, 𝐴, 𝐵) = 𝐴 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐴𝐹𝐶))
2 oveq1 6622 . 2 (if(𝜑, 𝐴, 𝐵) = 𝐵 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ifsb 4077 1 (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  ifcif 4064  (class class class)co 6615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618
This theorem is referenced by:  scmatscm  20259  pmatcollpwscmatlem1  20534  idpm2idmp  20546  monmat2matmon  20569  chmatval  20574  leibpi  24603  musumsum  24852  muinv  24853  dchrinvcl  24912  rpvmasum2  25135  padicabvcxp  25255  pnfneige0  29821  plymulx0  30446  ftc1anclem6  33161  linc0scn0  41530
  Copyright terms: Public domain W3C validator