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

Theorem ifan 3770
Description: Rewrite a conjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
Assertion
Ref Expression
ifan  |-  if ( ( ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)

Proof of Theorem ifan
StepHypRef Expression
1 iftrue 3737 . . 3  |-  ( ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)  =  if ( ps ,  A ,  B ) )
2 ibar 491 . . . 4  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
32ifbid 3749 . . 3  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ( ph  /\ 
ps ) ,  A ,  B ) )
41, 3eqtr2d 2468 . 2  |-  ( ph  ->  if ( ( ph  /\ 
ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
) )
5 simpl 444 . . . . 5  |-  ( (
ph  /\  ps )  ->  ph )
65con3i 129 . . . 4  |-  ( -. 
ph  ->  -.  ( ph  /\ 
ps ) )
7 iffalse 3738 . . . 4  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
86, 7syl 16 . . 3  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
9 iffalse 3738 . . 3  |-  ( -. 
ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B )  =  B )
108, 9eqtr4d 2470 . 2  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B ) )
114, 10pm2.61i 158 1  |-  if ( ( ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359    = wceq 1652   ifcif 3731
This theorem is referenced by:  itg0  19663  iblre  19677  itgreval  19680  iblss  19688  iblss2  19689  itgle  19693  itgss  19695  itgeqa  19697  iblconst  19701  itgconst  19702  ibladdlem  19703  iblabslem  19711  iblabsr  19713  iblmulc2  19714  itgsplit  19719  itgcn  19726  itg2gt0cn  26250  ibladdnclem  26251  iblabsnclem  26258  iblmulc2nc  26260  bddiblnc  26265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator