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

Theorem iftruei 3552
Description: Inference associated with iftrue 3551. (Contributed by BJ, 7-Oct-2018.)
Hypothesis
Ref Expression
iftruei.1  |-  ph
Assertion
Ref Expression
iftruei  |-  if (
ph ,  A ,  B )  =  A

Proof of Theorem iftruei
StepHypRef Expression
1 iftruei.1 . 2  |-  ph
2 iftrue 3551 . 2  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
31, 2ax-mp 5 1  |-  if (
ph ,  A ,  B )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1363   ifcif 3546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-if 3547
This theorem is referenced by:  ctmlemr  7121  xnegpnf  9842  xnegmnf  9843  xaddpnf1  9860  xaddpnf2  9861  xaddmnf1  9862  xaddmnf2  9863  pnfaddmnf  9864  mnfaddpnf  9865  iseqf1olemqk  10508  exp0  10538  sumsnf  11431  prodsnf  11614  lcm0val  12079  ennnfonelemj0  12416  ennnfonelem0  12420  mulg0  13020  lgs0  14710  lgs2  14714  peano3nninf  15053  dceqnconst  15105
  Copyright terms: Public domain W3C validator