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

Theorem ifan 4477
Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
Assertion
Ref Expression
ifan if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

Proof of Theorem ifan
StepHypRef Expression
1 iftrue 4430 . . 3 (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2 ibar 532 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32ifbid 4447 . . 3 (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑𝜓), 𝐴, 𝐵))
41, 3eqtr2d 2775 . 2 (𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5 simpl 486 . . . . 5 ((𝜑𝜓) → 𝜑)
65con3i 157 . . . 4 𝜑 → ¬ (𝜑𝜓))
76iffalsed 4435 . . 3 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = 𝐵)
8 iffalse 4433 . . 3 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
97, 8eqtr4d 2777 . 2 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
104, 9pm2.61i 185 1 if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399   = wceq 1542  ifcif 4424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-if 4425
This theorem is referenced by:  itg0  24544  iblre  24558  itgreval  24561  iblss  24569  iblss2  24570  itgle  24574  itgss  24576  itgeqa  24578  iblconst  24582  itgconst  24583  ibladdlem  24584  iblabslem  24592  iblabsr  24594  iblmulc2  24595  itgsplit  24600  bddiblnc  24606  itgcn  24609  mrsubrn  33058  itg2gt0cn  35487  ibladdnclem  35488  iblabsnclem  35495  iblmulc2nc  35497  iblsplit  43089
  Copyright terms: Public domain W3C validator