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 18	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  partfun  6684  mposnif  7528  tz7.44-3  8396  ttrcltr  9686  updjudhcoinlf  9919  iunfictbso  10099  ttukeylem7  10500  max0sub  13223  ifle  13224  xmulneg1  13296  xmulpnf1  13301  expnnval  14102  swrdval2  14686  swrdlend  14693  swrd0  14698  relexp0g  15061  max0add  15363  summolem2a  15768  prodmolem2a  15990  ef0lem  16133  rpnnen2lem3  16273  rpnnen2lem9  16279  iserodd  16896  pcmpt  16953  pcmpt2  16954  prmdvdsprmo  17103  fvprif  17616  setcepi  18146  gsumval2a  18744  smndex2dlinvh  18980  mgm2nsgrplem3  18983  mulgnn  19142  pmtrprfv  19524  pmtrprfval  19558  psgnunilem1  19564  dfod2  19635  oddvds2  19637  cyggenod  19955  fincygsubgodd  20185  ofldchr  21707  mplcoe1  22169  mplcoe5  22172  coe1tm  22415  coe1tmmul2fv  22420  coe1pwmulfv  22422  coe1sclmul  22424  coe1sclmul2  22426  m1detdiag  22735  mdetunilem9  22758  maducoeval2  22778  symgmatr01lem  22791  pmatcollpw3fi1lem1  22924  chpmat1dlem  22973  chfacffsupp  22994  chfacfscmul0  22996  chfacfpmmul0  23000  2ndcdisj  23594  dscmet  24710  xrsxmet  24948  cnmpopc  25068  xrhmeo  25086  oprpiece1res1  25091  htpycc  25120  pcoval1  25153  pcohtpylem  25159  pcoass  25164  pcorevlem  25166  ovolunlem1a  25636  ovolunlem1  25637  ovolicc2lem3  25659  ovolicc2lem4  25660  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  itg2const2  25881  itg2splitlem  25888  itg2split  25889  itg2cnlem1  25901  itg2cnlem2  25902  iblss2  25946  itgspliticc  25977  ditgpos  25996  limcres  26026  plyeq0lem  26348  plypf1  26350  coeeq2  26380  dvply1  26426  aareccl  26470  dvtaylp  26514  pserdvlem2  26572  lgamgulmlem4  27177  isppw  27259  vmappw  27261  muval1  27278  dchrelbasd  27384  dchr1  27402  dchrptlem2  27410  lgsdir2  27475  lgsne0  27480  gausslemma2dlem1a  27510  gausslemma2dlem2  27512  2sqnn0  27583  rplogsumlem2  27630  dchrisum0flblem2  27654  dchrisum0fno1  27656  rplogsum  27672  pntrlog2bndlem5  27726  noinfbnd2  27876  expnnsval  28600  1loopgrvd2  29834  1hevtxdg1  29837  1egrvtxdg1  29840  crctcshwlkn0lem2  30141  crctcshlem4  30150  crctcsh  30154  clwlkclwwlklem2fv1  30327  eulercrct  30574  eucrct2eupth  30577  ccatws1f1o  33252  pmtridfv1  33396  pmtridfv2  33397  psgnfzto1stlem  33401  elrgspnlem2  33544  elrgspnlem3  33545  elrspunsn  33718  gsummoncoe1fzo  33868  psrnzr  33883  0mplrim  33885  mplasclco  33887  evlextv  33913  esplyind  33946  vieta  33951  fldextrspunlsp  34045  extdgfialglem2  34064  rtelextdg2lem  34097  2sqr3minply  34151  smattl  34169  smattr  34170  smatbl  34171  1smat1  34175  madjusmdetlem1  34198  madjusmdetlem2  34199  esumpinfval  34444  eulerpartlemgs2  34751  ballotlemsgt1  34882  ballotlemsel1i  34884  ballotlemsi  34886  signswmnd  34925  signsvtn  34952  vonf1oonfo  35580  cvmliftlem10  35767  unblimceq0lem  37076  bj-rdg0gALT  37688  poimirlem1  38253  poimirlem2  38254  poimirlem5  38257  poimirlem6  38258  poimirlem12  38264  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  itg2addnc  38306  itg2gt0cn  38307  itgaddnclem2  38311  sdclem1  38375  cdlemefs27cl  41168  sticksstones9  42902  sticksstones10  42903  sticksstones12a  42905  unitscyglem1  42943  flcidc  43880  oe0suclim  43987  tfsconcatfv  44051  safesnsupfilb  44127  relexp01min  44422  relexpxpmin  44426  mnurnd  44976  ioondisj2  46192  ioondisj1  46193  lptioo1  46331  limsup10exlem  46469  icccncfext  46584  cncfiooicc  46591  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnxpaek  46639  ditgeq3d  46661  itgsubsticclem  46672  dirkerper  46793  dirkercncflem2  46801  fourierdlem40  46844  fourierdlem65  46868  fourierdlem74  46877  fourierdlem75  46878  fourierdlem78  46881  fourierdlem81  46884  fourierdlem97  46900  fourierdlem103  46906  fourierdlem104  46907  sqwvfoura  46925  sqwvfourb  46926  fourierswlem  46927  fouriersw  46928  elaa2lem  46930  etransclem19  46950  etransclem22  46953  etransclem24  46955  etransclem35  46966  sge0pnfval  47070  isomenndlem  47227  hoicvrrex  47253  ovn0  47263  volicon0  47272  hsphoidmvle2  47282  hsphoidmvle  47283  hoidmv1lelem1  47288  hoidmv1lelem2  47289  hoidmvlelem2  47293  hoidmvlelem3  47294  hspmbllem1  47323  hspmbllem2  47324  volico2  47338  ovolval2lem  47340  ovnsubadd2lem  47342  ovolval4lem1  47346  vonioolem1  47377  vonioo  47379  vonicclem1  47380  vonicc  47382  discsubc  49825  oppf1st2nd  49892  2oppf  49893  oppfval  49897