Theorem iftrued 4433

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

Syntax hints:   → wi 4   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  partfun  6503  mposnif  7304  tz7.44-3  8122  updjudhcoinlf  9513  iunfictbso  9693  ttukeylem7  10094  max0sub  12751  ifle  12752  xmulneg1  12824  xmulpnf1  12829  expnnval  13603  swrdval2  14176  swrdlend  14183  swrd0  14188  relexp0g  14550  max0add  14839  summolem2a  15244  prodmolem2a  15459  ef0lem  15603  rpnnen2lem3  15740  rpnnen2lem9  15746  iserodd  16351  pcmpt  16408  pcmpt2  16409  prmdvdsprmo  16558  fvprif  17020  setcepi  17548  gsumval2a  18111  smndex2dlinvh  18298  mgm2nsgrplem3  18301  mulgnn  18450  pmtrprfv  18799  pmtrprfval  18833  psgnunilem1  18839  dfod2  18909  oddvds2  18911  cyggenod  19222  fincygsubgodd  19453  mplcoe1  20948  mplcoe5  20951  coe1tm  21148  coe1tmmul2fv  21153  coe1pwmulfv  21155  coe1sclmul  21157  coe1sclmul2  21159  m1detdiag  21448  mdetunilem9  21471  maducoeval2  21491  symgmatr01lem  21504  pmatcollpw3fi1lem1  21637  chpmat1dlem  21686  chfacffsupp  21707  chfacfscmul0  21709  chfacfpmmul0  21713  2ndcdisj  22307  dscmet  23424  xrsxmet  23660  cnmpopc  23779  xrhmeo  23797  oprpiece1res1  23802  htpycc  23831  pcoval1  23864  pcohtpylem  23870  pcoass  23875  pcorevlem  23877  ovolunlem1a  24347  ovolunlem1  24348  ovolicc2lem3  24370  ovolicc2lem4  24371  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2const2  24593  itg2splitlem  24600  itg2split  24601  itg2cnlem1  24613  itg2cnlem2  24614  iblss2  24657  itgspliticc  24688  ditgpos  24707  limcres  24737  plyeq0lem  25058  plypf1  25060  coeeq2  25090  dvply1  25131  aareccl  25173  dvtaylp  25216  pserdvlem2  25274  lgamgulmlem4  25868  isppw  25950  vmappw  25952  muval1  25969  dchrelbasd  26074  dchr1  26092  dchrptlem2  26100  lgsdir2  26165  lgsne0  26170  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  2sqnn0  26273  rplogsumlem2  26320  dchrisum0flblem2  26344  dchrisum0fno1  26346  rplogsum  26362  pntrlog2bndlem5  26416  1loopgrvd2  27545  1hevtxdg1  27548  1egrvtxdg1  27551  crctcshwlkn0lem2  27849  crctcshlem4  27858  crctcsh  27862  clwlkclwwlklem2fv1  28032  eulercrct  28279  eucrct2eupth  28282  pmtridfv1  31035  pmtridfv2  31036  psgnfzto1stlem  31040  ofldchr  31186  smattl  31416  smattr  31417  smatbl  31418  1smat1  31422  madjusmdetlem1  31445  madjusmdetlem2  31446  esumpinfval  31707  eulerpartlemgs2  32013  ballotlemsgt1  32143  ballotlemsel1i  32145  ballotlemsi  32147  signswmnd  32202  signsvtn  32229  cvmliftlem10  32923  noinfbnd2  33620  unblimceq0lem  34372  poimirlem1  35464  poimirlem2  35465  poimirlem5  35468  poimirlem6  35469  poimirlem12  35475  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem23  35486  itg2addnc  35517  itg2gt0cn  35518  itgaddnclem2  35522  sdclem1  35587  cdlemefs27cl  38113  sticksstones9  39779  sticksstones10  39780  sticksstones12a  39782  metakunt5  39792  metakunt11  39798  metakunt21  39808  metakunt26  39813  metakunt27  39814  metakunt29  39816  metakunt30  39817  metakunt31  39818  flcidc  40643  relexp01min  40939  relexpxpmin  40943  mnurnd  41515  ioondisj2  42647  ioondisj1  42648  lptioo1  42791  limsup10exlem  42931  icccncfext  43046  cncfiooicc  43053  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnxpaek  43101  ditgeq3d  43123  itgsubsticclem  43134  dirkerper  43255  dirkercncflem2  43263  fourierdlem40  43306  fourierdlem65  43330  fourierdlem74  43339  fourierdlem75  43340  fourierdlem78  43343  fourierdlem81  43346  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  elaa2lem  43392  etransclem19  43412  etransclem22  43415  etransclem24  43417  etransclem35  43428  sge0pnfval  43529  isomenndlem  43686  hoicvrrex  43712  ovn0  43722  volicon0  43731  hsphoidmvle2  43741  hsphoidmvle  43742  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmvlelem2  43752  hoidmvlelem3  43753  hspmbllem1  43782  hspmbllem2  43783  volico2  43797  ovolval2lem  43799  ovnsubadd2lem  43801  ovolval4lem1  43805  vonioolem1  43836  vonioo  43838  vonicclem1  43839  vonicc  43841