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

Theorem iftrued 3400
Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
iftrued.1 (𝜑𝜒)
Assertion
Ref Expression
iftrued (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrued
StepHypRef Expression
1 iftrued.1 . 2 (𝜑𝜒)
2 iftrue 3398 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 14 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  ifcif 3393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-if 3394
This theorem is referenced by:  eqifdc  3425  fimax2gtrilemstep  6614  updjudhcoinlf  6769  fodjuomnilem0  6800  iseqf1olemnab  9913  iseqf1olemab  9914  iseqf1olemqk  9919  iseqf1olemfvp  9922  seq3f1olemqsumkj  9923  seq3f1olemqsum  9925  seq3f1oleml  9928  seq3f1o  9929  fser0const  9947  expnnval  9954  2zsupmax  10653  isummolem3  10766  isummolem2a  10767  iisum  10771  fisum  10774  isumss  10779  fsumcl2lem  10788  fsumadd  10796  fsummulc2  10838  cvgratz  10922  ef0lem  10946  gcdval  11225  ressid2  11546  nninfalllemn  11853  nninfsellemeq  11861  nninfsellemeqinf  11863
  Copyright terms: Public domain W3C validator