Theorem iftrued 4536

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  partfun  6695  mposnif  7521  tz7.44-3  8405  ttrcltr  9708  updjudhcoinlf  9924  iunfictbso  10106  ttukeylem7  10507  max0sub  13172  ifle  13173  xmulneg1  13245  xmulpnf1  13250  expnnval  14027  swrdval2  14593  swrdlend  14600  swrd0  14605  relexp0g  14966  max0add  15254  summolem2a  15658  prodmolem2a  15875  ef0lem  16019  rpnnen2lem3  16156  rpnnen2lem9  16162  iserodd  16765  pcmpt  16822  pcmpt2  16823  prmdvdsprmo  16972  fvprif  17504  setcepi  18035  gsumval2a  18601  smndex2dlinvh  18795  mgm2nsgrplem3  18798  mulgnn  18953  pmtrprfv  19316  pmtrprfval  19350  psgnunilem1  19356  dfod2  19427  oddvds2  19429  cyggenod  19747  fincygsubgodd  19977  mplcoe1  21584  mplcoe5  21587  coe1tm  21787  coe1tmmul2fv  21792  coe1pwmulfv  21794  coe1sclmul  21796  coe1sclmul2  21798  m1detdiag  22091  mdetunilem9  22114  maducoeval2  22134  symgmatr01lem  22147  pmatcollpw3fi1lem1  22280  chpmat1dlem  22329  chfacffsupp  22350  chfacfscmul0  22352  chfacfpmmul0  22356  2ndcdisj  22952  dscmet  24073  xrsxmet  24317  cnmpopc  24436  xrhmeo  24454  oprpiece1res1  24459  htpycc  24488  pcoval1  24521  pcohtpylem  24527  pcoass  24532  pcorevlem  24534  ovolunlem1a  25005  ovolunlem1  25006  ovolicc2lem3  25028  ovolicc2lem4  25029  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2const2  25251  itg2splitlem  25258  itg2split  25259  itg2cnlem1  25271  itg2cnlem2  25272  iblss2  25315  itgspliticc  25346  ditgpos  25365  limcres  25395  plyeq0lem  25716  plypf1  25718  coeeq2  25748  dvply1  25789  aareccl  25831  dvtaylp  25874  pserdvlem2  25932  lgamgulmlem4  26526  isppw  26608  vmappw  26610  muval1  26627  dchrelbasd  26732  dchr1  26750  dchrptlem2  26758  lgsdir2  26823  lgsne0  26828  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  2sqnn0  26931  rplogsumlem2  26978  dchrisum0flblem2  27002  dchrisum0fno1  27004  rplogsum  27020  pntrlog2bndlem5  27074  noinfbnd2  27224  1loopgrvd2  28750  1hevtxdg1  28753  1egrvtxdg1  28756  crctcshwlkn0lem2  29055  crctcshlem4  29064  crctcsh  29068  clwlkclwwlklem2fv1  29238  eulercrct  29485  eucrct2eupth  29488  pmtridfv1  32242  pmtridfv2  32243  psgnfzto1stlem  32247  ofldchr  32421  elrspunsn  32536  gsummoncoe1fzo  32657  smattl  32767  smattr  32768  smatbl  32769  1smat1  32773  madjusmdetlem1  32796  madjusmdetlem2  32797  esumpinfval  33060  eulerpartlemgs2  33368  ballotlemsgt1  33498  ballotlemsel1i  33500  ballotlemsi  33502  signswmnd  33557  signsvtn  33584  cvmliftlem10  34274  unblimceq0lem  35371  bj-rdg0gALT  35941  poimirlem1  36478  poimirlem2  36479  poimirlem5  36482  poimirlem6  36483  poimirlem12  36489  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  itg2addnc  36531  itg2gt0cn  36532  itgaddnclem2  36536  sdclem1  36600  cdlemefs27cl  39273  sticksstones9  40959  sticksstones10  40960  sticksstones12a  40962  metakunt5  40978  metakunt11  40984  metakunt21  40994  metakunt26  40999  metakunt27  41000  metakunt29  41002  metakunt30  41003  metakunt31  41004  flcidc  41902  oe0suclim  42013  tfsconcatfv  42077  safesnsupfilb  42155  relexp01min  42450  relexpxpmin  42454  mnurnd  43028  ioondisj2  44193  ioondisj1  44194  lptioo1  44335  limsup10exlem  44475  icccncfext  44590  cncfiooicc  44597  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnxpaek  44645  ditgeq3d  44667  itgsubsticclem  44678  dirkerper  44799  dirkercncflem2  44807  fourierdlem40  44850  fourierdlem65  44874  fourierdlem74  44883  fourierdlem75  44884  fourierdlem78  44887  fourierdlem81  44890  fourierdlem97  44906  fourierdlem103  44912  fourierdlem104  44913  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  elaa2lem  44936  etransclem19  44956  etransclem22  44959  etransclem24  44961  etransclem35  44972  sge0pnfval  45076  isomenndlem  45233  hoicvrrex  45259  ovn0  45269  volicon0  45278  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmvlelem2  45299  hoidmvlelem3  45300  hspmbllem1  45329  hspmbllem2  45330  volico2  45344  ovolval2lem  45346  ovnsubadd2lem  45348  ovolval4lem1  45352  vonioolem1  45383  vonioo  45385  vonicclem1  45386  vonicc  45388