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

Theorem ifan 3617
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 3584 . . 3  |-  ( ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)  =  if ( ps ,  A ,  B ) )
2 ibar 490 . . . 4  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
32ifbid 3596 . . 3  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ( ph  /\ 
ps ) ,  A ,  B ) )
41, 3eqtr2d 2329 . 2  |-  ( ph  ->  if ( ( ph  /\ 
ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
) )
5 simpl 443 . . . . 5  |-  ( (
ph  /\  ps )  ->  ph )
65con3i 127 . . . 4  |-  ( -. 
ph  ->  -.  ( ph  /\ 
ps ) )
7 iffalse 3585 . . . 4  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
86, 7syl 15 . . 3  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
9 iffalse 3585 . . 3  |-  ( -. 
ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B )  =  B )
108, 9eqtr4d 2331 . 2  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B ) )
114, 10pm2.61i 156 1  |-  if ( ( ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358    = wceq 1632   ifcif 3578
This theorem is referenced by:  itg0  19150  iblre  19164  itgreval  19167  iblss  19175  iblss2  19176  itgle  19180  itgss  19182  itgeqa  19184  iblconst  19188  itgconst  19189  ibladdlem  19190  iblabslem  19198  iblabsr  19200  iblmulc2  19201  itgsplit  19206  itgcn  19213  itg2gt0cn  25006  ibladdnclem  25007  iblabsnclem  25014  iblmulc2nc  25016  bddiblnc  25021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator