Theorem iftrued 4469

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

Syntax hints:   → wi 4   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  partfun  6639  mposnif  7479  tz7.44-3  8344  ttrcltr  9635  updjudhcoinlf  9854  iunfictbso  10034  ttukeylem7  10435  max0sub  13146  ifle  13147  xmulneg1  13219  xmulpnf1  13224  expnnval  14024  swrdval2  14607  swrdlend  14614  swrd0  14619  relexp0g  14982  max0add  15270  summolem2a  15675  prodmolem2a  15897  ef0lem  16041  rpnnen2lem3  16181  rpnnen2lem9  16187  iserodd  16804  pcmpt  16861  pcmpt2  16862  prmdvdsprmo  17011  fvprif  17523  setcepi  18053  gsumval2a  18651  smndex2dlinvh  18886  mgm2nsgrplem3  18889  mulgnn  19049  pmtrprfv  19426  pmtrprfval  19460  psgnunilem1  19466  dfod2  19537  oddvds2  19539  cyggenod  19857  fincygsubgodd  20087  ofldchr  21558  mplcoe1  22020  mplcoe5  22023  coe1tm  22266  coe1tmmul2fv  22271  coe1pwmulfv  22273  coe1sclmul  22275  coe1sclmul2  22277  m1detdiag  22587  mdetunilem9  22610  maducoeval2  22630  symgmatr01lem  22643  pmatcollpw3fi1lem1  22776  chpmat1dlem  22825  chfacffsupp  22846  chfacfscmul0  22848  chfacfpmmul0  22852  2ndcdisj  23446  dscmet  24562  xrsxmet  24800  cnmpopc  24920  xrhmeo  24938  oprpiece1res1  24943  htpycc  24972  pcoval1  25005  pcohtpylem  25011  pcoass  25016  pcorevlem  25018  ovolunlem1a  25488  ovolunlem1  25489  ovolicc2lem3  25511  ovolicc2lem4  25512  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  itg2const2  25733  itg2splitlem  25740  itg2split  25741  itg2cnlem1  25753  itg2cnlem2  25754  iblss2  25798  itgspliticc  25829  ditgpos  25848  limcres  25878  plyeq0lem  26200  plypf1  26202  coeeq2  26232  dvply1  26275  aareccl  26317  dvtaylp  26360  pserdvlem2  26418  lgamgulmlem4  27020  isppw  27102  vmappw  27104  muval1  27121  dchrelbasd  27227  dchr1  27245  dchrptlem2  27253  lgsdir2  27318  lgsne0  27323  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  2sqnn0  27426  rplogsumlem2  27473  dchrisum0flblem2  27497  dchrisum0fno1  27499  rplogsum  27515  pntrlog2bndlem5  27569  noinfbnd2  27720  expnnsval  28443  1loopgrvd2  29597  1hevtxdg1  29600  1egrvtxdg1  29603  crctcshwlkn0lem2  29904  crctcshlem4  29913  crctcsh  29917  clwlkclwwlklem2fv1  30090  eulercrct  30337  eucrct2eupth  30340  ccatws1f1o  33037  pmtridfv1  33183  pmtridfv2  33184  psgnfzto1stlem  33188  elrgspnlem2  33331  elrgspnlem3  33332  elrspunsn  33519  gsummoncoe1fzo  33687  psrnzr  33703  0mplrim  33705  mplasclco  33707  evlextv  33733  esplyind  33766  vieta  33771  fldextrspunlsp  33865  extdgfialglem2  33884  rtelextdg2lem  33917  2sqr3minply  33971  smattl  33989  smattr  33990  smatbl  33991  1smat1  33995  madjusmdetlem1  34018  madjusmdetlem2  34019  esumpinfval  34264  eulerpartlemgs2  34571  ballotlemsgt1  34702  ballotlemsel1i  34704  ballotlemsi  34706  signswmnd  34748  signsvtn  34775  cvmliftlem10  35529  unblimceq0lem  36819  bj-rdg0gALT  37431  poimirlem1  37995  poimirlem2  37996  poimirlem5  37999  poimirlem6  38000  poimirlem12  38006  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  itg2addnc  38048  itg2gt0cn  38049  itgaddnclem2  38053  sdclem1  38117  cdlemefs27cl  40912  sticksstones9  42646  sticksstones10  42647  sticksstones12a  42649  unitscyglem1  42687  flcidc  43622  oe0suclim  43729  tfsconcatfv  43793  safesnsupfilb  43869  relexp01min  44164  relexpxpmin  44168  mnurnd  44734  ioondisj2  45945  ioondisj1  45946  lptioo1  46084  limsup10exlem  46222  icccncfext  46337  cncfiooicc  46344  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  ditgeq3d  46414  itgsubsticclem  46425  dirkerper  46546  dirkercncflem2  46554  fourierdlem40  46597  fourierdlem65  46621  fourierdlem74  46630  fourierdlem75  46631  fourierdlem78  46634  fourierdlem81  46637  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  elaa2lem  46683  etransclem19  46703  etransclem22  46706  etransclem24  46708  etransclem35  46719  sge0pnfval  46823  isomenndlem  46980  hoicvrrex  47006  ovn0  47016  volicon0  47025  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmvlelem2  47046  hoidmvlelem3  47047  hspmbllem1  47076  hspmbllem2  47077  volico2  47091  ovolval2lem  47093  ovnsubadd2lem  47095  ovolval4lem1  47099  vonioolem1  47130  vonioo  47132  vonicclem1  47133  vonicc  47135  discsubc  49561  oppf1st2nd  49628  2oppf  49629  oppfval  49633