Theorem iftrued 4500

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

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 ⊢ (𝜑 → 𝜒)
2		iftrue 4498	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4493

This theorem is used by:  partfun  6689  mposnif  7539  tz7.44-3  8404  ttrcltr  9695  updjudhcoinlf  9937  iunfictbso  10117  ttukeylem7  10517  max0sub  13240  ifle  13241  xmulneg1  13313  xmulpnf1  13318  expnnval  14120  swrdval2  14706  swrdlend  14715  swrd0  14720  relexp0g  15085  max0add  15387  summolem2a  15792  prodmolem2a  16014  ef0lem  16157  rpnnen2lem3  16297  rpnnen2lem9  16303  sadadd2lem2  16533  iserodd  16920  pcmpt  16977  pcmpt2  16978  prmdvdsprmo  17127  fvprif  17640  setcepi  18170  gsumval2a  18772  smndex2dlinvh  19010  mgm2nsgrplem3  19013  mulgnn  19172  pmtrprfv  19554  pmtrprfval  19588  psgnunilem1  19594  dfod2  19665  oddvds2  19667  cyggenod  19985  fincygsubgodd  20215  ofldchr  21763  mplcoe1  22225  mplcoe5  22228  coe1tm  22471  coe1tmmul2fv  22476  coe1pwmulfv  22478  coe1sclmul  22480  coe1sclmul2  22482  m1detdiag  22791  mdetunilem9  22814  maducoeval2  22834  symgmatr01lem  22847  pmatcollpw3fi1lem1  22980  chpmat1dlem  23029  chfacffsupp  23050  chfacfscmul0  23052  chfacfpmmul0  23056  2ndcdisj  23650  dscmet  24766  xrsxmet  25004  cnmpopc  25124  xrhmeo  25142  oprpiece1res1  25147  htpycc  25176  pcoval1  25209  pcohtpylem  25215  pcoass  25220  pcorevlem  25222  ovolunlem1a  25692  ovolunlem1  25693  ovolicc2lem3  25715  ovolicc2lem4  25716  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1fseqlem6  25916  itg2const2  25937  itg2splitlem  25944  itg2split  25945  itg2cnlem1  25957  itg2cnlem2  25958  iblss2  26002  itgspliticc  26033  ditgpos  26052  limcres  26082  plyeq0lem  26404  plypf1  26406  coeeq2  26436  dvply1  26482  aareccl  26526  dvtaylp  26570  pserdvlem2  26628  lgamgulmlem4  27233  isppw  27315  vmappw  27317  muval1  27334  dchrelbasd  27440  dchr1  27458  dchrptlem2  27466  lgsdir2  27531  lgsne0  27536  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  2sqnn0  27639  rplogsumlem2  27686  dchrisum0flblem2  27710  dchrisum0fno1  27712  rplogsum  27728  pntrlog2bndlem5  27782  noinfbnd2  27932  expnnsval  28656  1loopgrvd2  29890  1hevtxdg1  29893  1egrvtxdg1  29896  crctcshwlkn0lem2  30197  crctcshlem4  30206  crctcsh  30210  clwlkclwwlklem2fv1  30383  eulercrct  30630  eucrct2eupth  30633  ccatws1f1o  33304  pmtridfv1  33446  pmtridfv2  33447  psgnfzto1stlem  33451  elrgspnlem2  33594  elrgspnlem3  33595  elrspunsn  33768  gsummoncoe1fzo  33918  psrnzr  33933  0mplrim  33935  mplasclco  33937  evlextv  33963  esplyind  33996  vieta  34001  fldextrspunlsp  34095  extdgfialglem2  34114  rtelextdg2lem  34147  2sqr3minply  34201  smattl  34219  smattr  34220  smatbl  34221  1smat1  34225  madjusmdetlem1  34248  madjusmdetlem2  34249  esumpinfval  34494  eulerpartlemgs2  34802  ballotlemsgt1  34933  ballotlemsel1i  34935  ballotlemsi  34937  signswmnd  34976  signsvtn  35003  vonf1oonfo  35623  cvmliftlem10  35807  unblimceq0lem  37136  bj-rdg0gALT  37748  poimirlem1  38313  poimirlem2  38314  poimirlem5  38317  poimirlem6  38318  poimirlem12  38324  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  itg2addnc  38366  itg2gt0cn  38367  itgaddnclem2  38371  sdclem1  38435  cdlemefs27cl  41228  sticksstones9  42962  sticksstones10  42963  sticksstones12a  42965  unitscyglem1  43003  flcidc  43938  oe0suclim  44045  tfsconcatfv  44109  safesnsupfilb  44185  relexp01min  44480  relexpxpmin  44484  mnurnd  45034  ioondisj2  46250  ioondisj1  46251  lptioo1  46389  limsup10exlem  46527  icccncfext  46642  cncfiooicc  46649  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnxpaek  46697  ditgeq3d  46719  itgsubsticclem  46730  dirkerper  46851  dirkercncflem2  46859  fourierdlem40  46902  fourierdlem65  46926  fourierdlem74  46935  fourierdlem75  46936  fourierdlem78  46939  fourierdlem81  46942  fourierdlem97  46958  fourierdlem103  46964  fourierdlem104  46965  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  elaa2lem  46988  etransclem19  47008  etransclem22  47011  etransclem24  47013  etransclem35  47024  sge0pnfval  47128  isomenndlem  47285  hoicvrrex  47311  ovn0  47321  volicon0  47330  hsphoidmvle2  47340  hsphoidmvle  47341  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmvlelem2  47351  hoidmvlelem3  47352  hspmbllem1  47381  hspmbllem2  47382  volico2  47396  ovolval2lem  47398  ovnsubadd2lem  47400  ovolval4lem1  47404  vonioolem1  47435  vonioo  47437  vonicclem1  47438  vonicc  47440  discsubc  49883  oppf1st2nd  49950  2oppf  49951  oppfval  49955