ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ifsbdc Unicode version

Theorem ifsbdc 3532
Description: Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.)
Hypotheses
Ref Expression
ifsbdc.1  |-  ( if ( ph ,  A ,  B )  =  A  ->  C  =  D )
ifsbdc.2  |-  ( if ( ph ,  A ,  B )  =  B  ->  C  =  E )
Assertion
Ref Expression
ifsbdc  |-  (DECID  ph  ->  C  =  if ( ph ,  D ,  E ) )

Proof of Theorem ifsbdc
StepHypRef Expression
1 exmiddc 826 . 2  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)
2 iftrue 3525 . . . . 5  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
3 ifsbdc.1 . . . . 5  |-  ( if ( ph ,  A ,  B )  =  A  ->  C  =  D )
42, 3syl 14 . . . 4  |-  ( ph  ->  C  =  D )
5 iftrue 3525 . . . 4  |-  ( ph  ->  if ( ph ,  D ,  E )  =  D )
64, 5eqtr4d 2201 . . 3  |-  ( ph  ->  C  =  if (
ph ,  D ,  E ) )
7 iffalse 3528 . . . . 5  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
8 ifsbdc.2 . . . . 5  |-  ( if ( ph ,  A ,  B )  =  B  ->  C  =  E )
97, 8syl 14 . . . 4  |-  ( -. 
ph  ->  C  =  E )
10 iffalse 3528 . . . 4  |-  ( -. 
ph  ->  if ( ph ,  D ,  E )  =  E )
119, 10eqtr4d 2201 . . 3  |-  ( -. 
ph  ->  C  =  if ( ph ,  D ,  E ) )
126, 11jaoi 706 . 2  |-  ( (
ph  \/  -.  ph )  ->  C  =  if (
ph ,  D ,  E ) )
131, 12syl 14 1  |-  (DECID  ph  ->  C  =  if ( ph ,  D ,  E ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 698  DECID wdc 824    = wceq 1343   ifcif 3520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-dc 825  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-if 3521
This theorem is referenced by:  fvifdc  5508  lgsneg  13565  lgsdilem  13568
  Copyright terms: Public domain W3C validator