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

Theorem ifan 4577
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 4530 . . 3 (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2 ibar 528 . . . 4 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32ifbid 4547 . . 3 (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑𝜓), 𝐴, 𝐵))
41, 3eqtr2d 2768 . 2 (𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5 simpl 482 . . . . 5 ((𝜑𝜓) → 𝜑)
65con3i 154 . . . 4 𝜑 → ¬ (𝜑𝜓))
76iffalsed 4535 . . 3 𝜑 → if((𝜑𝜓), 𝐴, 𝐵) = 𝐵)
8 iffalse 4533 . . 3 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
97, 8eqtr4d 2770 . 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 1534  ifcif 4524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-if 4525
This theorem is referenced by:  itg0  25696  iblre  25710  itgreval  25713  iblss  25721  iblss2  25722  itgle  25726  itgss  25728  itgeqa  25730  iblconst  25734  itgconst  25735  ibladdlem  25736  iblabslem  25744  iblabsr  25746  iblmulc2  25747  itgsplit  25752  bddiblnc  25758  itgcn  25761  mrsubrn  35059  itg2gt0cn  37083  ibladdnclem  37084  iblabsnclem  37091  iblmulc2nc  37093  selvvvval  41740  iblsplit  45277
  Copyright terms: Public domain W3C validator