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

Theorem ifan 4580
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 4533 . . 3 (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2 ibar 530 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32ifbid 4550 . . 3 (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑𝜓), 𝐴, 𝐵))
41, 3eqtr2d 2774 . 2 (𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5 simpl 484 . . . . 5 ((𝜑𝜓) → 𝜑)
65con3i 154 . . . 4 𝜑 → ¬ (𝜑𝜓))
76iffalsed 4538 . . 3 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = 𝐵)
8 iffalse 4536 . . 3 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
97, 8eqtr4d 2776 . 2 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
104, 9pm2.61i 182 1 if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397   = wceq 1542  ifcif 4527
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4528
This theorem is referenced by:  itg0  25279  iblre  25293  itgreval  25296  iblss  25304  iblss2  25305  itgle  25309  itgss  25311  itgeqa  25313  iblconst  25317  itgconst  25318  ibladdlem  25319  iblabslem  25327  iblabsr  25329  iblmulc2  25330  itgsplit  25335  bddiblnc  25341  itgcn  25344  mrsubrn  34442  itg2gt0cn  36481  ibladdnclem  36482  iblabsnclem  36489  iblmulc2nc  36491  selvvvval  41107  iblsplit  44617
  Copyright terms: Public domain W3C validator