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

Theorem ifan 3985
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 3945 . . 3  |-  ( ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)  =  if ( ps ,  A ,  B ) )
2 ibar 504 . . . 4  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
32ifbid 3961 . . 3  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ( ph  /\ 
ps ) ,  A ,  B ) )
41, 3eqtr2d 2509 . 2  |-  ( ph  ->  if ( ( ph  /\ 
ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
) )
5 simpl 457 . . . . 5  |-  ( (
ph  /\  ps )  ->  ph )
65con3i 135 . . . 4  |-  ( -. 
ph  ->  -.  ( ph  /\ 
ps ) )
7 iffalse 3948 . . . 4  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
86, 7syl 16 . . 3  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  B )
9 iffalse 3948 . . 3  |-  ( -. 
ph  ->  if ( ph ,  if ( ps ,  A ,  B ) ,  B )  =  B )
108, 9eqtr4d 2511 . 2  |-  ( -. 
ph  ->  if ( (
ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B ) )
114, 10pm2.61i 164 1  |-  if ( ( ph  /\  ps ) ,  A ,  B )  =  if ( ph ,  if ( ps ,  A ,  B ) ,  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  itg0  22013  iblre  22027  itgreval  22030  iblss  22038  iblss2  22039  itgle  22043  itgss  22045  itgeqa  22047  iblconst  22051  itgconst  22052  ibladdlem  22053  iblabslem  22061  iblabsr  22063  iblmulc2  22064  itgsplit  22069  itgcn  22076  mrsubrn  28624  itg2gt0cn  29923  ibladdnclem  29924  iblabsnclem  29931  iblmulc2nc  29933  bddiblnc  29938  iblsplit  31511
  Copyright terms: Public domain W3C validator