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

Theorem ifan 4512
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 4465 . . 3 (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2 ibar 529 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32ifbid 4482 . . 3 (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑𝜓), 𝐴, 𝐵))
41, 3eqtr2d 2779 . 2 (𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5 simpl 483 . . . . 5 ((𝜑𝜓) → 𝜑)
65con3i 154 . . . 4 𝜑 → ¬ (𝜑𝜓))
76iffalsed 4470 . . 3 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = 𝐵)
8 iffalse 4468 . . 3 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
97, 8eqtr4d 2781 . 2 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
104, 9pm2.61i 182 1 if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 396   = wceq 1539  ifcif 4459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460
This theorem is referenced by:  itg0  24944  iblre  24958  itgreval  24961  iblss  24969  iblss2  24970  itgle  24974  itgss  24976  itgeqa  24978  iblconst  24982  itgconst  24983  ibladdlem  24984  iblabslem  24992  iblabsr  24994  iblmulc2  24995  itgsplit  25000  bddiblnc  25006  itgcn  25009  mrsubrn  33475  itg2gt0cn  35832  ibladdnclem  35833  iblabsnclem  35840  iblmulc2nc  35842  iblsplit  43507
  Copyright terms: Public domain W3C validator