Theorem iftrued 4493

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 4491	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

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

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  partfun  6683  mposnif  7533  tz7.44-3  8401  ttrcltr  9699  updjudhcoinlf  9941  iunfictbso  10121  ttukeylem7  10521  max0sub  13252  ifle  13253  xmulneg1  13325  xmulpnf1  13330  expnnval  14132  swrdval2  14718  swrdlend  14727  swrd0  14732  relexp0g  15099  max0add  15401  summolem2a  15805  prodmolem2a  16027  ef0lem  16170  rpnnen2lem3  16310  rpnnen2lem9  16316  sadadd2lem2  16546  iserodd  16933  pcmpt  16990  pcmpt2  16991  prmdvdsprmo  17140  fvprif  17653  setcepi  18183  gsumval2a  18793  smndex2dlinvh  19035  mgm2nsgrplem3  19038  mulgnn  19204  pmtrprfv  19586  pmtrprfval  19620  psgnunilem1  19626  dfod2  19697  oddvds2  19699  cyggenod  20017  fincygsubgodd  20247  ofldchr  21795  mplcoe1  22259  mplcoe5  22262  coe1tm  22505  coe1tmmul2fv  22510  coe1pwmulfv  22512  coe1sclmul  22514  coe1sclmul2  22516  m1detdiag  22825  mdetunilem9  22848  maducoeval2  22868  symgmatr01lem  22881  pmatcollpw3fi1lem1  23017  chpmat1dlem  23066  chfacffsupp  23087  chfacfscmul0  23089  chfacfpmmul0  23093  2ndcdisj  23688  dscmet  24804  xrsxmet  25042  cnmpopc  25162  xrhmeo  25180  oprpiece1res1  25185  htpycc  25214  pcoval1  25247  pcohtpylem  25253  pcoass  25258  pcorevlem  25260  ovolunlem1a  25730  ovolunlem1  25731  ovolicc2lem3  25753  ovolicc2lem4  25754  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1fseqlem6  25954  itg2const2  25975  itg2splitlem  25982  itg2split  25983  itg2cnlem1  25995  itg2cnlem2  25996  iblss2  26040  itgspliticc  26071  ditgpos  26090  limcres  26120  plyeq0lem  26443  plypf1  26445  coeeq2  26475  dvply1  26521  aareccl  26569  dvtaylp  26613  pserdvlem2  26671  lgamgulmlem4  27276  isppw  27358  vmappw  27360  muval1  27377  dchrelbasd  27483  dchr1  27501  dchrptlem2  27509  lgsdir2  27574  lgsne0  27579  gausslemma2dlem1a  27609  gausslemma2dlem2  27611  2sqnn0  27682  rplogsumlem2  27729  dchrisum0flblem2  27753  dchrisum0fno1  27755  rplogsum  27771  pntrlog2bndlem5  27825  noinfbnd2  27975  expnnsval  28699  angmgmaddov2  29276  1loopgrvd2  29971  1hevtxdg1  29974  1egrvtxdg1  29977  crctcshwlkn0lem2  30287  crctcshlem4  30296  crctcsh  30300  clwlkclwwlklem2fv1  30473  eulercrct  30730  eucrct2eupth  30733  ccatws1f1o  33401  pmtridfv1  33543  pmtridfv2  33544  psgnfzto1stlem  33548  elrgspnlem2  33691  elrgspnlem3  33692  elrspunsn  33865  gsummoncoe1fzo  34015  psrnzr  34030  0mplrim  34032  mplasclco  34034  evlextv  34060  esplyind  34093  vieta  34098  fldextrspunlsp  34192  extdgfialglem2  34211  rtelextdg2lem  34244  2sqr3minply  34298  smattl  34316  smattr  34317  smatbl  34318  1smat1  34322  madjusmdetlem1  34345  madjusmdetlem2  34346  esumpinfval  34591  eulerpartlemgs2  34899  ballotlemsgt1  35030  ballotlemsel1i  35032  ballotlemsi  35034  signswmnd  35073  signsvtn  35100  vonf1oonfo  35720  cvmliftlem10  35881  unblimceq0lem  37211  bj-rdg0gALT  37823  poimirlem1  38378  poimirlem2  38379  poimirlem5  38382  poimirlem6  38383  poimirlem12  38389  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  itg2addnc  38431  itg2gt0cn  38432  itgaddnclem2  38436  sdclem1  38501  cdlemefs27cl  41294  sticksstones9  43028  sticksstones10  43029  sticksstones12a  43031  unitscyglem1  43069  flcidc  44019  oe0suclim  44126  tfsconcatfv  44190  safesnsupfilb  44266  relexp01min  44561  relexpxpmin  44565  mnurnd  45115  ioondisj2  46331  ioondisj1  46332  lptioo1  46470  limsup10exlem  46608  icccncfext  46723  cncfiooicc  46730  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnxpaek  46778  ditgeq3d  46800  itgsubsticclem  46811  dirkerper  46932  dirkercncflem2  46940  fourierdlem40  46983  fourierdlem65  47007  fourierdlem74  47016  fourierdlem75  47017  fourierdlem78  47020  fourierdlem81  47023  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  elaa2lem  47069  etransclem19  47089  etransclem22  47092  etransclem24  47094  etransclem35  47105  sge0pnfval  47209  isomenndlem  47366  hoicvrrex  47392  ovn0  47402  volicon0  47411  hsphoidmvle2  47421  hsphoidmvle  47422  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmvlelem2  47432  hoidmvlelem3  47433  hspmbllem1  47462  hspmbllem2  47463  volico2  47477  ovolval2lem  47479  ovnsubadd2lem  47481  ovolval4lem1  47485  vonioolem1  47516  vonioo  47518  vonicclem1  47519  vonicc  47521  tmachlem-agreeprod  47773  discsubc  49998  oppf1st2nd  50065  2oppf  50066  oppfval  50070