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

Theorem iftrued 3449
Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
iftrued.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
iftrued  |-  ( ph  ->  if ( ch ,  A ,  B )  =  A )

Proof of Theorem iftrued
StepHypRef Expression
1 iftrued.1 . 2  |-  ( ph  ->  ch )
2 iftrue 3447 . 2  |-  ( ch 
->  if ( ch ,  A ,  B )  =  A )
31, 2syl 14 1  |-  ( ph  ->  if ( ch ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   ifcif 3442
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 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-if 3443
This theorem is referenced by:  eqifdc  3474  mposnif  5831  fimax2gtrilemstep  6760  updjudhcoinlf  6931  omp1eomlem  6945  difinfsnlem  6950  ctssdclemn0  6961  ctssdc  6964  enumctlemm  6965  fodju0  6985  iseqf1olemnab  10212  iseqf1olemab  10213  iseqf1olemqk  10218  iseqf1olemfvp  10221  seq3f1olemqsumkj  10222  seq3f1olemqsum  10224  seq3f1oleml  10227  seq3f1o  10228  fser0const  10240  expnnval  10247  2zsupmax  10948  xrmaxifle  10966  xrmaxiflemab  10967  xrmaxiflemlub  10968  xrmaxiflemcom  10969  summodclem3  11100  summodclem2a  11101  isum  11105  fsum3  11107  isumss  11111  fsumcl2lem  11118  fsumadd  11126  fsummulc2  11168  cvgratz  11252  ef0lem  11276  gcdval  11555  ennnfonelemss  11829  ennnfonelemkh  11831  ennnfonelemhf1o  11832  ressid2  11924  subctctexmid  13030  nninfalllemn  13036  nninfsellemeq  13044  nninfsellemeqinf  13046  nninffeq  13050
  Copyright terms: Public domain W3C validator