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

Theorem ifan 4583
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 4536 . . 3 (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2 ibar 528 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32ifbid 4553 . . 3 (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑𝜓), 𝐴, 𝐵))
41, 3eqtr2d 2775 . 2 (𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5 simpl 482 . . . . 5 ((𝜑𝜓) → 𝜑)
65con3i 154 . . . 4 𝜑 → ¬ (𝜑𝜓))
76iffalsed 4541 . . 3 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = 𝐵)
8 iffalse 4539 . . 3 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
97, 8eqtr4d 2777 . 2 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
104, 9pm2.61i 182 1 if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1536  ifcif 4530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531
This theorem is referenced by:  itg0  25829  iblre  25843  itgreval  25846  iblss  25854  iblss2  25855  itgle  25859  itgss  25861  itgeqa  25863  iblconst  25867  itgconst  25868  ibladdlem  25869  iblabslem  25877  iblabsr  25879  iblmulc2  25880  itgsplit  25885  bddiblnc  25891  itgcn  25894  mrsubrn  35497  itg2gt0cn  37661  ibladdnclem  37662  iblabsnclem  37669  iblmulc2nc  37671  selvvvval  42571  iblsplit  45921
  Copyright terms: Public domain W3C validator