Theorem iftrued 4496

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4488

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  partfun  6665  mposnif  7505  tz7.44-3  8376  ttrcltr  9669  updjudhcoinlf  9885  iunfictbso  10067  ttukeylem7  10468  max0sub  13156  ifle  13157  xmulneg1  13229  xmulpnf1  13234  expnnval  14029  swrdval2  14611  swrdlend  14618  swrd0  14623  relexp0g  14988  max0add  15276  summolem2a  15681  prodmolem2a  15900  ef0lem  16044  rpnnen2lem3  16184  rpnnen2lem9  16190  iserodd  16806  pcmpt  16863  pcmpt2  16864  prmdvdsprmo  17013  fvprif  17524  setcepi  18050  gsumval2a  18612  smndex2dlinvh  18844  mgm2nsgrplem3  18847  mulgnn  19007  pmtrprfv  19383  pmtrprfval  19417  psgnunilem1  19423  dfod2  19494  oddvds2  19496  cyggenod  19814  fincygsubgodd  20044  mplcoe1  21944  mplcoe5  21947  coe1tm  22159  coe1tmmul2fv  22164  coe1pwmulfv  22166  coe1sclmul  22168  coe1sclmul2  22170  m1detdiag  22484  mdetunilem9  22507  maducoeval2  22527  symgmatr01lem  22540  pmatcollpw3fi1lem1  22673  chpmat1dlem  22722  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  2ndcdisj  23343  dscmet  24460  xrsxmet  24698  cnmpopc  24822  xrhmeo  24844  oprpiece1res1  24849  htpycc  24879  pcoval1  24913  pcohtpylem  24919  pcoass  24924  pcorevlem  24926  ovolunlem1a  25397  ovolunlem1  25398  ovolicc2lem3  25420  ovolicc2lem4  25421  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2const2  25642  itg2splitlem  25649  itg2split  25650  itg2cnlem1  25662  itg2cnlem2  25663  iblss2  25707  itgspliticc  25738  ditgpos  25757  limcres  25787  plyeq0lem  26115  plypf1  26117  coeeq2  26147  dvply1  26191  aareccl  26234  dvtaylp  26278  pserdvlem2  26338  lgamgulmlem4  26942  isppw  27024  vmappw  27026  muval1  27043  dchrelbasd  27150  dchr1  27168  dchrptlem2  27176  lgsdir2  27241  lgsne0  27246  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  2sqnn0  27349  rplogsumlem2  27396  dchrisum0flblem2  27420  dchrisum0fno1  27422  rplogsum  27438  pntrlog2bndlem5  27492  noinfbnd2  27643  expsnnval  28312  1loopgrvd2  29431  1hevtxdg1  29434  1egrvtxdg1  29437  crctcshwlkn0lem2  29741  crctcshlem4  29750  crctcsh  29754  clwlkclwwlklem2fv1  29924  eulercrct  30171  eucrct2eupth  30174  ccatws1f1o  32873  pmtridfv1  33052  pmtridfv2  33053  psgnfzto1stlem  33057  elrgspnlem2  33194  elrgspnlem3  33195  ofldchr  33292  elrspunsn  33400  gsummoncoe1fzo  33563  fldextrspunlsp  33669  rtelextdg2lem  33716  2sqr3minply  33770  smattl  33788  smattr  33789  smatbl  33790  1smat1  33794  madjusmdetlem1  33817  madjusmdetlem2  33818  esumpinfval  34063  eulerpartlemgs2  34371  ballotlemsgt1  34502  ballotlemsel1i  34504  ballotlemsi  34506  signswmnd  34548  signsvtn  34575  cvmliftlem10  35281  unblimceq0lem  36494  bj-rdg0gALT  37059  poimirlem1  37615  poimirlem2  37616  poimirlem5  37619  poimirlem6  37620  poimirlem12  37626  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  itg2addnc  37668  itg2gt0cn  37669  itgaddnclem2  37673  sdclem1  37737  cdlemefs27cl  40407  sticksstones9  42142  sticksstones10  42143  sticksstones12a  42145  unitscyglem1  42183  flcidc  43159  oe0suclim  43266  tfsconcatfv  43330  safesnsupfilb  43407  relexp01min  43702  relexpxpmin  43706  mnurnd  44272  ioondisj2  45491  ioondisj1  45492  lptioo1  45630  limsup10exlem  45770  icccncfext  45885  cncfiooicc  45892  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  ditgeq3d  45962  itgsubsticclem  45973  dirkerper  46094  dirkercncflem2  46102  fourierdlem40  46145  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem81  46185  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem19  46251  etransclem22  46254  etransclem24  46256  etransclem35  46267  sge0pnfval  46371  isomenndlem  46528  hoicvrrex  46554  ovn0  46564  volicon0  46573  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmvlelem2  46594  hoidmvlelem3  46595  hspmbllem1  46624  hspmbllem2  46625  volico2  46639  ovolval2lem  46641  ovnsubadd2lem  46643  ovolval4lem1  46647  vonioolem1  46678  vonioo  46680  vonicclem1  46681  vonicc  46683  discsubc  49053  oppf1st2nd  49120  2oppf  49121  oppfval  49125