Theorem iftrued 4535

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4527

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4528

This theorem is referenced by:  partfun  6696  mposnif  7526  tz7.44-3  8410  ttrcltr  9713  updjudhcoinlf  9929  iunfictbso  10111  ttukeylem7  10512  max0sub  13179  ifle  13180  xmulneg1  13252  xmulpnf1  13257  expnnval  14034  swrdval2  14600  swrdlend  14607  swrd0  14612  relexp0g  14973  max0add  15261  summolem2a  15665  prodmolem2a  15882  ef0lem  16026  rpnnen2lem3  16163  rpnnen2lem9  16169  iserodd  16772  pcmpt  16829  pcmpt2  16830  prmdvdsprmo  16979  fvprif  17511  setcepi  18042  gsumval2a  18610  smndex2dlinvh  18834  mgm2nsgrplem3  18837  mulgnn  18994  pmtrprfv  19362  pmtrprfval  19396  psgnunilem1  19402  dfod2  19473  oddvds2  19475  cyggenod  19793  fincygsubgodd  20023  mplcoe1  21811  mplcoe5  21814  coe1tm  22015  coe1tmmul2fv  22020  coe1pwmulfv  22022  coe1sclmul  22024  coe1sclmul2  22026  m1detdiag  22319  mdetunilem9  22342  maducoeval2  22362  symgmatr01lem  22375  pmatcollpw3fi1lem1  22508  chpmat1dlem  22557  chfacffsupp  22578  chfacfscmul0  22580  chfacfpmmul0  22584  2ndcdisj  23180  dscmet  24301  xrsxmet  24545  cnmpopc  24669  xrhmeo  24691  oprpiece1res1  24696  htpycc  24726  pcoval1  24760  pcohtpylem  24766  pcoass  24771  pcorevlem  24773  ovolunlem1a  25245  ovolunlem1  25246  ovolicc2lem3  25268  ovolicc2lem4  25269  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  mbfi1fseqlem6  25470  itg2const2  25491  itg2splitlem  25498  itg2split  25499  itg2cnlem1  25511  itg2cnlem2  25512  iblss2  25555  itgspliticc  25586  ditgpos  25605  limcres  25635  plyeq0lem  25959  plypf1  25961  coeeq2  25991  dvply1  26033  aareccl  26075  dvtaylp  26118  pserdvlem2  26176  lgamgulmlem4  26772  isppw  26854  vmappw  26856  muval1  26873  dchrelbasd  26978  dchr1  26996  dchrptlem2  27004  lgsdir2  27069  lgsne0  27074  gausslemma2dlem1a  27104  gausslemma2dlem2  27106  2sqnn0  27177  rplogsumlem2  27224  dchrisum0flblem2  27248  dchrisum0fno1  27250  rplogsum  27266  pntrlog2bndlem5  27320  noinfbnd2  27470  1loopgrvd2  29027  1hevtxdg1  29030  1egrvtxdg1  29033  crctcshwlkn0lem2  29332  crctcshlem4  29341  crctcsh  29345  clwlkclwwlklem2fv1  29515  eulercrct  29762  eucrct2eupth  29765  pmtridfv1  32524  pmtridfv2  32525  psgnfzto1stlem  32529  ofldchr  32702  elrspunsn  32821  gsummoncoe1fzo  32943  smattl  33076  smattr  33077  smatbl  33078  1smat1  33082  madjusmdetlem1  33105  madjusmdetlem2  33106  esumpinfval  33369  eulerpartlemgs2  33677  ballotlemsgt1  33807  ballotlemsel1i  33809  ballotlemsi  33811  signswmnd  33866  signsvtn  33893  cvmliftlem10  34583  unblimceq0lem  35685  bj-rdg0gALT  36255  poimirlem1  36792  poimirlem2  36793  poimirlem5  36796  poimirlem6  36797  poimirlem12  36803  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem22  36813  poimirlem23  36814  itg2addnc  36845  itg2gt0cn  36846  itgaddnclem2  36850  sdclem1  36914  cdlemefs27cl  39587  sticksstones9  41276  sticksstones10  41277  sticksstones12a  41279  metakunt5  41295  metakunt11  41301  metakunt21  41311  metakunt26  41316  metakunt27  41317  metakunt29  41319  metakunt30  41320  metakunt31  41321  flcidc  42218  oe0suclim  42329  tfsconcatfv  42393  safesnsupfilb  42471  relexp01min  42766  relexpxpmin  42770  mnurnd  43344  ioondisj2  44504  ioondisj1  44505  lptioo1  44646  limsup10exlem  44786  icccncfext  44901  cncfiooicc  44908  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnxpaek  44956  ditgeq3d  44978  itgsubsticclem  44989  dirkerper  45110  dirkercncflem2  45118  fourierdlem40  45161  fourierdlem65  45185  fourierdlem74  45194  fourierdlem75  45195  fourierdlem78  45198  fourierdlem81  45201  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  elaa2lem  45247  etransclem19  45267  etransclem22  45270  etransclem24  45272  etransclem35  45283  sge0pnfval  45387  isomenndlem  45544  hoicvrrex  45570  ovn0  45580  volicon0  45589  hsphoidmvle2  45599  hsphoidmvle  45600  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmvlelem2  45610  hoidmvlelem3  45611  hspmbllem1  45640  hspmbllem2  45641  volico2  45655  ovolval2lem  45657  ovnsubadd2lem  45659  ovolval4lem1  45663  vonioolem1  45694  vonioo  45696  vonicclem1  45697  vonicc  45699