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

Theorem ifan 3778
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 3745 . . 3  |-  ( ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)  =  if ( ps ,  A ,  B ) )
2 ibar 491 . . . 4  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
32ifbid 3757 . . 3  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ( ph  /\ 
ps ) ,  A ,  B ) )
41, 3eqtr2d 2469 . 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 3746 . . . 4  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
86, 7syl 16 . . 3  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
9 iffalse 3746 . . 3  |-  ( -. 
ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B )  =  B )
108, 9eqtr4d 2471 . 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 3739
This theorem is referenced by:  itg0  19671  iblre  19685  itgreval  19688  iblss  19696  iblss2  19697  itgle  19701  itgss  19703  itgeqa  19705  iblconst  19709  itgconst  19710  ibladdlem  19711  iblabslem  19719  iblabsr  19721  iblmulc2  19722  itgsplit  19727  itgcn  19734  itg2gt0cn  26260  ibladdnclem  26261  iblabsnclem  26268  iblmulc2nc  26270  bddiblnc  26275
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-if 3740
  Copyright terms: Public domain W3C validator