Theorem iftrued 4539

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  partfun  6716  mposnif  7549  tz7.44-3  8447  ttrcltr  9754  updjudhcoinlf  9970  iunfictbso  10152  ttukeylem7  10553  max0sub  13235  ifle  13236  xmulneg1  13308  xmulpnf1  13313  expnnval  14102  swrdval2  14681  swrdlend  14688  swrd0  14693  relexp0g  15058  max0add  15346  summolem2a  15748  prodmolem2a  15967  ef0lem  16111  rpnnen2lem3  16249  rpnnen2lem9  16255  iserodd  16869  pcmpt  16926  pcmpt2  16927  prmdvdsprmo  17076  fvprif  17608  setcepi  18142  gsumval2a  18711  smndex2dlinvh  18943  mgm2nsgrplem3  18946  mulgnn  19106  pmtrprfv  19486  pmtrprfval  19520  psgnunilem1  19526  dfod2  19597  oddvds2  19599  cyggenod  19917  fincygsubgodd  20147  mplcoe1  22073  mplcoe5  22076  coe1tm  22292  coe1tmmul2fv  22297  coe1pwmulfv  22299  coe1sclmul  22301  coe1sclmul2  22303  m1detdiag  22619  mdetunilem9  22642  maducoeval2  22662  symgmatr01lem  22675  pmatcollpw3fi1lem1  22808  chpmat1dlem  22857  chfacffsupp  22878  chfacfscmul0  22880  chfacfpmmul0  22884  2ndcdisj  23480  dscmet  24601  xrsxmet  24845  cnmpopc  24969  xrhmeo  24991  oprpiece1res1  24996  htpycc  25026  pcoval1  25060  pcohtpylem  25066  pcoass  25071  pcorevlem  25073  ovolunlem1a  25545  ovolunlem1  25546  ovolicc2lem3  25568  ovolicc2lem4  25569  mbfi1fseqlem4  25768  mbfi1fseqlem5  25769  mbfi1fseqlem6  25770  itg2const2  25791  itg2splitlem  25798  itg2split  25799  itg2cnlem1  25811  itg2cnlem2  25812  iblss2  25856  itgspliticc  25887  ditgpos  25906  limcres  25936  plyeq0lem  26264  plypf1  26266  coeeq2  26296  dvply1  26340  aareccl  26383  dvtaylp  26427  pserdvlem2  26487  lgamgulmlem4  27090  isppw  27172  vmappw  27174  muval1  27191  dchrelbasd  27298  dchr1  27316  dchrptlem2  27324  lgsdir2  27389  lgsne0  27394  gausslemma2dlem1a  27424  gausslemma2dlem2  27426  2sqnn0  27497  rplogsumlem2  27544  dchrisum0flblem2  27568  dchrisum0fno1  27570  rplogsum  27586  pntrlog2bndlem5  27640  noinfbnd2  27791  expsnnval  28424  1loopgrvd2  29536  1hevtxdg1  29539  1egrvtxdg1  29542  crctcshwlkn0lem2  29841  crctcshlem4  29850  crctcsh  29854  clwlkclwwlklem2fv1  30024  eulercrct  30271  eucrct2eupth  30274  ccatws1f1o  32921  pmtridfv1  33098  pmtridfv2  33099  psgnfzto1stlem  33103  elrgspnlem2  33233  elrgspnlem3  33234  ofldchr  33324  elrspunsn  33437  gsummoncoe1fzo  33598  rtelextdg2lem  33732  2sqr3minply  33753  smattl  33759  smattr  33760  smatbl  33761  1smat1  33765  madjusmdetlem1  33788  madjusmdetlem2  33789  esumpinfval  34054  eulerpartlemgs2  34362  ballotlemsgt1  34492  ballotlemsel1i  34494  ballotlemsi  34496  signswmnd  34551  signsvtn  34578  cvmliftlem10  35279  unblimceq0lem  36489  bj-rdg0gALT  37054  poimirlem1  37608  poimirlem2  37609  poimirlem5  37612  poimirlem6  37613  poimirlem12  37619  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  itg2addnc  37661  itg2gt0cn  37662  itgaddnclem2  37666  sdclem1  37730  cdlemefs27cl  40396  sticksstones9  42136  sticksstones10  42137  sticksstones12a  42139  unitscyglem1  42177  metakunt5  42191  metakunt11  42197  metakunt21  42207  metakunt26  42212  metakunt27  42213  metakunt29  42215  metakunt30  42216  metakunt31  42217  flcidc  43159  oe0suclim  43267  tfsconcatfv  43331  safesnsupfilb  43408  relexp01min  43703  relexpxpmin  43707  mnurnd  44279  ioondisj2  45446  ioondisj1  45447  lptioo1  45588  limsup10exlem  45728  icccncfext  45843  cncfiooicc  45850  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  dvnxpaek  45898  ditgeq3d  45920  itgsubsticclem  45931  dirkerper  46052  dirkercncflem2  46060  fourierdlem40  46103  fourierdlem65  46127  fourierdlem74  46136  fourierdlem75  46137  fourierdlem78  46140  fourierdlem81  46143  fourierdlem97  46159  fourierdlem103  46165  fourierdlem104  46166  sqwvfoura  46184  sqwvfourb  46185  fourierswlem  46186  fouriersw  46187  elaa2lem  46189  etransclem19  46209  etransclem22  46212  etransclem24  46214  etransclem35  46225  sge0pnfval  46329  isomenndlem  46486  hoicvrrex  46512  ovn0  46522  volicon0  46531  hsphoidmvle2  46541  hsphoidmvle  46542  hoidmv1lelem1  46547  hoidmv1lelem2  46548  hoidmvlelem2  46552  hoidmvlelem3  46553  hspmbllem1  46582  hspmbllem2  46583  volico2  46597  ovolval2lem  46599  ovnsubadd2lem  46601  ovolval4lem1  46605  vonioolem1  46636  vonioo  46638  vonicclem1  46639  vonicc  46641