Theorem iftrued 4499

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  partfun  6668  mposnif  7508  tz7.44-3  8379  ttrcltr  9676  updjudhcoinlf  9892  iunfictbso  10074  ttukeylem7  10475  max0sub  13163  ifle  13164  xmulneg1  13236  xmulpnf1  13241  expnnval  14036  swrdval2  14618  swrdlend  14625  swrd0  14630  relexp0g  14995  max0add  15283  summolem2a  15688  prodmolem2a  15907  ef0lem  16051  rpnnen2lem3  16191  rpnnen2lem9  16197  iserodd  16813  pcmpt  16870  pcmpt2  16871  prmdvdsprmo  17020  fvprif  17531  setcepi  18057  gsumval2a  18619  smndex2dlinvh  18851  mgm2nsgrplem3  18854  mulgnn  19014  pmtrprfv  19390  pmtrprfval  19424  psgnunilem1  19430  dfod2  19501  oddvds2  19503  cyggenod  19821  fincygsubgodd  20051  mplcoe1  21951  mplcoe5  21954  coe1tm  22166  coe1tmmul2fv  22171  coe1pwmulfv  22173  coe1sclmul  22175  coe1sclmul2  22177  m1detdiag  22491  mdetunilem9  22514  maducoeval2  22534  symgmatr01lem  22547  pmatcollpw3fi1lem1  22680  chpmat1dlem  22729  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  2ndcdisj  23350  dscmet  24467  xrsxmet  24705  cnmpopc  24829  xrhmeo  24851  oprpiece1res1  24856  htpycc  24886  pcoval1  24920  pcohtpylem  24926  pcoass  24931  pcorevlem  24933  ovolunlem1a  25404  ovolunlem1  25405  ovolicc2lem3  25427  ovolicc2lem4  25428  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2const2  25649  itg2splitlem  25656  itg2split  25657  itg2cnlem1  25669  itg2cnlem2  25670  iblss2  25714  itgspliticc  25745  ditgpos  25764  limcres  25794  plyeq0lem  26122  plypf1  26124  coeeq2  26154  dvply1  26198  aareccl  26241  dvtaylp  26285  pserdvlem2  26345  lgamgulmlem4  26949  isppw  27031  vmappw  27033  muval1  27050  dchrelbasd  27157  dchr1  27175  dchrptlem2  27183  lgsdir2  27248  lgsne0  27253  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  2sqnn0  27356  rplogsumlem2  27403  dchrisum0flblem2  27427  dchrisum0fno1  27429  rplogsum  27445  pntrlog2bndlem5  27499  noinfbnd2  27650  expsnnval  28319  1loopgrvd2  29438  1hevtxdg1  29441  1egrvtxdg1  29444  crctcshwlkn0lem2  29748  crctcshlem4  29757  crctcsh  29761  clwlkclwwlklem2fv1  29931  eulercrct  30178  eucrct2eupth  30181  ccatws1f1o  32880  pmtridfv1  33059  pmtridfv2  33060  psgnfzto1stlem  33064  elrgspnlem2  33201  elrgspnlem3  33202  ofldchr  33299  elrspunsn  33407  gsummoncoe1fzo  33570  fldextrspunlsp  33676  rtelextdg2lem  33723  2sqr3minply  33777  smattl  33795  smattr  33796  smatbl  33797  1smat1  33801  madjusmdetlem1  33824  madjusmdetlem2  33825  esumpinfval  34070  eulerpartlemgs2  34378  ballotlemsgt1  34509  ballotlemsel1i  34511  ballotlemsi  34513  signswmnd  34555  signsvtn  34582  cvmliftlem10  35288  unblimceq0lem  36501  bj-rdg0gALT  37066  poimirlem1  37622  poimirlem2  37623  poimirlem5  37626  poimirlem6  37627  poimirlem12  37633  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  itg2addnc  37675  itg2gt0cn  37676  itgaddnclem2  37680  sdclem1  37744  cdlemefs27cl  40414  sticksstones9  42149  sticksstones10  42150  sticksstones12a  42152  unitscyglem1  42190  flcidc  43166  oe0suclim  43273  tfsconcatfv  43337  safesnsupfilb  43414  relexp01min  43709  relexpxpmin  43713  mnurnd  44279  ioondisj2  45498  ioondisj1  45499  lptioo1  45637  limsup10exlem  45777  icccncfext  45892  cncfiooicc  45899  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  ditgeq3d  45969  itgsubsticclem  45980  dirkerper  46101  dirkercncflem2  46109  fourierdlem40  46152  fourierdlem65  46176  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem81  46192  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem19  46258  etransclem22  46261  etransclem24  46263  etransclem35  46274  sge0pnfval  46378  isomenndlem  46535  hoicvrrex  46561  ovn0  46571  volicon0  46580  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmvlelem2  46601  hoidmvlelem3  46602  hspmbllem1  46631  hspmbllem2  46632  volico2  46646  ovolval2lem  46648  ovnsubadd2lem  46650  ovolval4lem1  46654  vonioolem1  46685  vonioo  46687  vonicclem1  46688  vonicc  46690  discsubc  49057  oppf1st2nd  49124  2oppf  49125  oppfval  49129