Theorem iftrued 4483

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  partfun  6628  mposnif  7462  tz7.44-3  8327  ttrcltr  9606  updjudhcoinlf  9822  iunfictbso  10002  ttukeylem7  10403  max0sub  13092  ifle  13093  xmulneg1  13165  xmulpnf1  13170  expnnval  13968  swrdval2  14551  swrdlend  14558  swrd0  14563  relexp0g  14926  max0add  15214  summolem2a  15619  prodmolem2a  15838  ef0lem  15982  rpnnen2lem3  16122  rpnnen2lem9  16128  iserodd  16744  pcmpt  16801  pcmpt2  16802  prmdvdsprmo  16951  fvprif  17462  setcepi  17992  gsumval2a  18590  smndex2dlinvh  18822  mgm2nsgrplem3  18825  mulgnn  18985  pmtrprfv  19363  pmtrprfval  19397  psgnunilem1  19403  dfod2  19474  oddvds2  19476  cyggenod  19794  fincygsubgodd  20024  ofldchr  21511  mplcoe1  21970  mplcoe5  21973  coe1tm  22185  coe1tmmul2fv  22190  coe1pwmulfv  22192  coe1sclmul  22194  coe1sclmul2  22196  m1detdiag  22510  mdetunilem9  22533  maducoeval2  22553  symgmatr01lem  22566  pmatcollpw3fi1lem1  22699  chpmat1dlem  22748  chfacffsupp  22769  chfacfscmul0  22771  chfacfpmmul0  22775  2ndcdisj  23369  dscmet  24485  xrsxmet  24723  cnmpopc  24847  xrhmeo  24869  oprpiece1res1  24874  htpycc  24904  pcoval1  24938  pcohtpylem  24944  pcoass  24949  pcorevlem  24951  ovolunlem1a  25422  ovolunlem1  25423  ovolicc2lem3  25445  ovolicc2lem4  25446  mbfi1fseqlem4  25644  mbfi1fseqlem5  25645  mbfi1fseqlem6  25646  itg2const2  25667  itg2splitlem  25674  itg2split  25675  itg2cnlem1  25687  itg2cnlem2  25688  iblss2  25732  itgspliticc  25763  ditgpos  25782  limcres  25812  plyeq0lem  26140  plypf1  26142  coeeq2  26172  dvply1  26216  aareccl  26259  dvtaylp  26303  pserdvlem2  26363  lgamgulmlem4  26967  isppw  27049  vmappw  27051  muval1  27068  dchrelbasd  27175  dchr1  27193  dchrptlem2  27201  lgsdir2  27266  lgsne0  27271  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  2sqnn0  27374  rplogsumlem2  27421  dchrisum0flblem2  27445  dchrisum0fno1  27447  rplogsum  27463  pntrlog2bndlem5  27517  noinfbnd2  27668  expsnnval  28347  1loopgrvd2  29480  1hevtxdg1  29483  1egrvtxdg1  29486  crctcshwlkn0lem2  29787  crctcshlem4  29796  crctcsh  29800  clwlkclwwlklem2fv1  29970  eulercrct  30217  eucrct2eupth  30220  ccatws1f1o  32927  pmtridfv1  33059  pmtridfv2  33060  psgnfzto1stlem  33064  elrgspnlem2  33205  elrgspnlem3  33206  elrspunsn  33389  gsummoncoe1fzo  33553  fldextrspunlsp  33682  extdgfialglem2  33701  rtelextdg2lem  33734  2sqr3minply  33788  smattl  33806  smattr  33807  smatbl  33808  1smat1  33812  madjusmdetlem1  33835  madjusmdetlem2  33836  esumpinfval  34081  eulerpartlemgs2  34388  ballotlemsgt1  34519  ballotlemsel1i  34521  ballotlemsi  34523  signswmnd  34565  signsvtn  34592  cvmliftlem10  35326  unblimceq0lem  36539  bj-rdg0gALT  37104  poimirlem1  37660  poimirlem2  37661  poimirlem5  37664  poimirlem6  37665  poimirlem12  37671  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  itg2addnc  37713  itg2gt0cn  37714  itgaddnclem2  37718  sdclem1  37782  cdlemefs27cl  40451  sticksstones9  42186  sticksstones10  42187  sticksstones12a  42189  unitscyglem1  42227  flcidc  43202  oe0suclim  43309  tfsconcatfv  43373  safesnsupfilb  43450  relexp01min  43745  relexpxpmin  43749  mnurnd  44315  ioondisj2  45532  ioondisj1  45533  lptioo1  45671  limsup10exlem  45809  icccncfext  45924  cncfiooicc  45931  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnxpaek  45979  ditgeq3d  46001  itgsubsticclem  46012  dirkerper  46133  dirkercncflem2  46141  fourierdlem40  46184  fourierdlem65  46208  fourierdlem74  46217  fourierdlem75  46218  fourierdlem78  46221  fourierdlem81  46224  fourierdlem97  46240  fourierdlem103  46246  fourierdlem104  46247  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  elaa2lem  46270  etransclem19  46290  etransclem22  46293  etransclem24  46295  etransclem35  46306  sge0pnfval  46410  isomenndlem  46567  hoicvrrex  46593  ovn0  46603  volicon0  46612  hsphoidmvle2  46622  hsphoidmvle  46623  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmvlelem2  46633  hoidmvlelem3  46634  hspmbllem1  46663  hspmbllem2  46664  volico2  46678  ovolval2lem  46680  ovnsubadd2lem  46682  ovolval4lem1  46686  vonioolem1  46717  vonioo  46719  vonicclem1  46720  vonicc  46722  discsubc  49095  oppf1st2nd  49162  2oppf  49163  oppfval  49167