Theorem iftrued 4491

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

Syntax hints:   → wi 4   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  partfun  6672  mposnif  7516  tz7.44-3  8383  ttrcltr  9673  updjudhcoinlf  9906  iunfictbso  10086  ttukeylem7  10487  max0sub  13210  ifle  13211  xmulneg1  13283  xmulpnf1  13288  expnnval  14088  swrdval2  14672  swrdlend  14679  swrd0  14684  relexp0g  15047  max0add  15349  summolem2a  15754  prodmolem2a  15976  ef0lem  16120  rpnnen2lem3  16260  rpnnen2lem9  16266  iserodd  16883  pcmpt  16940  pcmpt2  16941  prmdvdsprmo  17090  fvprif  17603  setcepi  18133  gsumval2a  18731  smndex2dlinvh  18967  mgm2nsgrplem3  18970  mulgnn  19129  pmtrprfv  19511  pmtrprfval  19545  psgnunilem1  19551  dfod2  19622  oddvds2  19624  cyggenod  19942  fincygsubgodd  20172  ofldchr  21683  mplcoe1  22145  mplcoe5  22148  coe1tm  22391  coe1tmmul2fv  22396  coe1pwmulfv  22398  coe1sclmul  22400  coe1sclmul2  22402  m1detdiag  22711  mdetunilem9  22734  maducoeval2  22754  symgmatr01lem  22767  pmatcollpw3fi1lem1  22900  chpmat1dlem  22949  chfacffsupp  22970  chfacfscmul0  22972  chfacfpmmul0  22976  2ndcdisj  23570  dscmet  24686  xrsxmet  24924  cnmpopc  25044  xrhmeo  25062  oprpiece1res1  25067  htpycc  25096  pcoval1  25129  pcohtpylem  25135  pcoass  25140  pcorevlem  25142  ovolunlem1a  25612  ovolunlem1  25613  ovolicc2lem3  25635  ovolicc2lem4  25636  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfi1fseqlem6  25836  itg2const2  25857  itg2splitlem  25864  itg2split  25865  itg2cnlem1  25877  itg2cnlem2  25878  iblss2  25922  itgspliticc  25953  ditgpos  25972  limcres  26002  plyeq0lem  26324  plypf1  26326  coeeq2  26356  dvply1  26402  aareccl  26444  dvtaylp  26487  pserdvlem2  26545  lgamgulmlem4  27150  isppw  27232  vmappw  27234  muval1  27251  dchrelbasd  27357  dchr1  27375  dchrptlem2  27383  lgsdir2  27448  lgsne0  27453  gausslemma2dlem1a  27483  gausslemma2dlem2  27485  2sqnn0  27556  rplogsumlem2  27603  dchrisum0flblem2  27627  dchrisum0fno1  27629  rplogsum  27645  pntrlog2bndlem5  27699  noinfbnd2  27849  expnnsval  28573  1loopgrvd2  29758  1hevtxdg1  29761  1egrvtxdg1  29764  crctcshwlkn0lem2  30065  crctcshlem4  30074  crctcsh  30078  clwlkclwwlklem2fv1  30251  eulercrct  30498  eucrct2eupth  30501  ccatws1f1o  33179  pmtridfv1  33323  pmtridfv2  33324  psgnfzto1stlem  33328  elrgspnlem2  33471  elrgspnlem3  33472  elrspunsn  33648  gsummoncoe1fzo  33799  psrnzr  33814  0mplrim  33816  mplasclco  33818  evlextv  33844  esplyind  33877  vieta  33882  fldextrspunlsp  33976  extdgfialglem2  33995  rtelextdg2lem  34028  2sqr3minply  34082  smattl  34100  smattr  34101  smatbl  34102  1smat1  34106  madjusmdetlem1  34129  madjusmdetlem2  34130  esumpinfval  34375  eulerpartlemgs2  34682  ballotlemsgt1  34813  ballotlemsel1i  34815  ballotlemsi  34817  signswmnd  34856  signsvtn  34883  vonf1oonfo  35465  cvmliftlem10  35652  unblimceq0lem  36952  bj-rdg0gALT  37563  poimirlem1  38127  poimirlem2  38128  poimirlem5  38131  poimirlem6  38132  poimirlem12  38138  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  itg2addnc  38180  itg2gt0cn  38181  itgaddnclem2  38185  sdclem1  38249  cdlemefs27cl  41044  sticksstones9  42778  sticksstones10  42779  sticksstones12a  42781  unitscyglem1  42819  flcidc  43754  oe0suclim  43861  tfsconcatfv  43925  safesnsupfilb  44001  relexp01min  44296  relexpxpmin  44300  mnurnd  44852  ioondisj2  46068  ioondisj1  46069  lptioo1  46207  limsup10exlem  46345  icccncfext  46460  cncfiooicc  46467  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnxpaek  46515  ditgeq3d  46537  itgsubsticclem  46548  dirkerper  46669  dirkercncflem2  46677  fourierdlem40  46720  fourierdlem65  46744  fourierdlem74  46753  fourierdlem75  46754  fourierdlem78  46757  fourierdlem81  46760  fourierdlem97  46776  fourierdlem103  46782  fourierdlem104  46783  sqwvfoura  46801  sqwvfourb  46802  fourierswlem  46803  fouriersw  46804  elaa2lem  46806  etransclem19  46826  etransclem22  46829  etransclem24  46831  etransclem35  46842  sge0pnfval  46946  isomenndlem  47103  hoicvrrex  47129  ovn0  47139  volicon0  47148  hsphoidmvle2  47158  hsphoidmvle  47159  hoidmv1lelem1  47164  hoidmv1lelem2  47165  hoidmvlelem2  47169  hoidmvlelem3  47170  hspmbllem1  47199  hspmbllem2  47200  volico2  47214  ovolval2lem  47216  ovnsubadd2lem  47218  ovolval4lem1  47222  vonioolem1  47253  vonioo  47255  vonicclem1  47256  vonicc  47258  discsubc  49694  oppf1st2nd  49761  2oppf  49762  oppfval  49766