Theorem iftrued 4474

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  partfun  6645  mposnif  7483  tz7.44-3  8347  ttrcltr  9637  updjudhcoinlf  9856  iunfictbso  10036  ttukeylem7  10437  max0sub  13148  ifle  13149  xmulneg1  13221  xmulpnf1  13226  expnnval  14026  swrdval2  14609  swrdlend  14616  swrd0  14621  relexp0g  14984  max0add  15272  summolem2a  15677  prodmolem2a  15899  ef0lem  16043  rpnnen2lem3  16183  rpnnen2lem9  16189  iserodd  16806  pcmpt  16863  pcmpt2  16864  prmdvdsprmo  17013  fvprif  17525  setcepi  18055  gsumval2a  18653  smndex2dlinvh  18888  mgm2nsgrplem3  18891  mulgnn  19051  pmtrprfv  19428  pmtrprfval  19462  psgnunilem1  19468  dfod2  19539  oddvds2  19541  cyggenod  19859  fincygsubgodd  20089  ofldchr  21556  mplcoe1  22015  mplcoe5  22018  coe1tm  22238  coe1tmmul2fv  22243  coe1pwmulfv  22245  coe1sclmul  22247  coe1sclmul2  22249  m1detdiag  22562  mdetunilem9  22585  maducoeval2  22605  symgmatr01lem  22618  pmatcollpw3fi1lem1  22751  chpmat1dlem  22800  chfacffsupp  22821  chfacfscmul0  22823  chfacfpmmul0  22827  2ndcdisj  23421  dscmet  24537  xrsxmet  24775  cnmpopc  24895  xrhmeo  24913  oprpiece1res1  24918  htpycc  24947  pcoval1  24980  pcohtpylem  24986  pcoass  24991  pcorevlem  24993  ovolunlem1a  25463  ovolunlem1  25464  ovolicc2lem3  25486  ovolicc2lem4  25487  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2const2  25708  itg2splitlem  25715  itg2split  25716  itg2cnlem1  25728  itg2cnlem2  25729  iblss2  25773  itgspliticc  25804  ditgpos  25823  limcres  25853  plyeq0lem  26175  plypf1  26177  coeeq2  26207  dvply1  26250  aareccl  26292  dvtaylp  26335  pserdvlem2  26393  lgamgulmlem4  26995  isppw  27077  vmappw  27079  muval1  27096  dchrelbasd  27202  dchr1  27220  dchrptlem2  27228  lgsdir2  27293  lgsne0  27298  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  2sqnn0  27401  rplogsumlem2  27448  dchrisum0flblem2  27472  dchrisum0fno1  27474  rplogsum  27490  pntrlog2bndlem5  27544  noinfbnd2  27695  expnnsval  28418  1loopgrvd2  29572  1hevtxdg1  29575  1egrvtxdg1  29578  crctcshwlkn0lem2  29879  crctcshlem4  29888  crctcsh  29892  clwlkclwwlklem2fv1  30065  eulercrct  30312  eucrct2eupth  30315  ccatws1f1o  33011  pmtridfv1  33156  pmtridfv2  33157  psgnfzto1stlem  33161  elrgspnlem2  33304  elrgspnlem3  33305  elrspunsn  33489  gsummoncoe1fzo  33657  evlextv  33686  esplyind  33719  vieta  33724  fldextrspunlsp  33818  extdgfialglem2  33837  rtelextdg2lem  33870  2sqr3minply  33924  smattl  33942  smattr  33943  smatbl  33944  1smat1  33948  madjusmdetlem1  33971  madjusmdetlem2  33972  esumpinfval  34217  eulerpartlemgs2  34524  ballotlemsgt1  34655  ballotlemsel1i  34657  ballotlemsi  34659  signswmnd  34701  signsvtn  34728  cvmliftlem10  35476  unblimceq0lem  36766  bj-rdg0gALT  37378  poimirlem1  37942  poimirlem2  37943  poimirlem5  37946  poimirlem6  37947  poimirlem12  37953  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  itg2addnc  37995  itg2gt0cn  37996  itgaddnclem2  38000  sdclem1  38064  cdlemefs27cl  40859  sticksstones9  42593  sticksstones10  42594  sticksstones12a  42596  unitscyglem1  42634  flcidc  43598  oe0suclim  43705  tfsconcatfv  43769  safesnsupfilb  43845  relexp01min  44140  relexpxpmin  44144  mnurnd  44710  ioondisj2  45923  ioondisj1  45924  lptioo1  46062  limsup10exlem  46200  icccncfext  46315  cncfiooicc  46322  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  ditgeq3d  46392  itgsubsticclem  46403  dirkerper  46524  dirkercncflem2  46532  fourierdlem40  46575  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem81  46615  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem19  46681  etransclem22  46684  etransclem24  46686  etransclem35  46697  sge0pnfval  46801  isomenndlem  46958  hoicvrrex  46984  ovn0  46994  volicon0  47003  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmvlelem2  47024  hoidmvlelem3  47025  hspmbllem1  47054  hspmbllem2  47055  volico2  47069  ovolval2lem  47071  ovnsubadd2lem  47073  ovolval4lem1  47077  vonioolem1  47108  vonioo  47110  vonicclem1  47111  vonicc  47113  discsubc  49539  oppf1st2nd  49606  2oppf  49607  oppfval  49611