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

Theorem ifan 3929
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 3889 . . 3  |-  ( ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)  =  if ( ps ,  A ,  B ) )
2 ibar 507 . . . 4  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
32ifbid 3905 . . 3  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ( ph  /\ 
ps ) ,  A ,  B ) )
41, 3eqtr2d 2488 . 2  |-  ( ph  ->  if ( ( ph  /\ 
ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
) )
5 simpl 459 . . . . 5  |-  ( (
ph  /\  ps )  ->  ph )
65con3i 141 . . . 4  |-  ( -. 
ph  ->  -.  ( ph  /\ 
ps ) )
76iffalsed 3894 . . 3  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
8 iffalse 3892 . . 3  |-  ( -. 
ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B )  =  B )
97, 8eqtr4d 2490 . 2  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B ) )
104, 9pm2.61i 168 1  |-  if ( ( ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 371    = wceq 1446   ifcif 3883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3884
This theorem is referenced by:  itg0  22749  iblre  22763  itgreval  22766  iblss  22774  iblss2  22775  itgle  22779  itgss  22781  itgeqa  22783  iblconst  22787  itgconst  22788  ibladdlem  22789  iblabslem  22797  iblabsr  22799  iblmulc2  22800  itgsplit  22805  itgcn  22812  mrsubrn  30163  itg2gt0cn  32009  ibladdnclem  32010  iblabsnclem  32017  iblmulc2nc  32019  bddiblnc  32024  iblsplit  37853
  Copyright terms: Public domain W3C validator