Theorem iftrued 4493

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  partfun  6716  mposnif  7567  tz7.44-3  8454  ttrcltr  9754  updjudhcoinlf  10050  iunfictbso  10232  ttukeylem7  10632  max0sub  13366  ifle  13367  xmulneg1  13439  xmulpnf1  13444  expnnval  14247  swrdval2  14836  swrdlend  14845  swrd0  14850  relexp0g  15218  max0add  15520  summolem2a  15925  prodmolem2a  16145  ef0lem  16288  rpnnen2lem3  16428  rpnnen2lem9  16434  sadadd2lem2  16664  iserodd  17057  pcmpt  17114  pcmpt2  17115  prmdvdsprmo  17264  fvprif  17783  setcepi  18313  gsumval2a  18924  smndex2dlinvh  19166  mgm2nsgrplem3  19169  mulgnn  19335  pmtrprfv  19718  pmtrprfval  19752  psgnunilem1  19758  dfod2  19829  oddvds2  19831  cyggenod  20149  fincygsubgodd  20379  ofldchr  21937  mplcoe1  22401  mplcoe5  22404  coe1tm  22647  coe1tmmul2fv  22652  coe1pwmulfv  22654  coe1sclmul  22656  coe1sclmul2  22658  m1detdiag  22967  mdetunilem9  22990  maducoeval2  23010  symgmatr01lem  23023  pmatcollpw3fi1lem1  23159  chpmat1dlem  23208  chfacffsupp  23229  chfacfscmul0  23231  chfacfpmmul0  23235  2ndcdisj  23830  dscmet  24946  xrsxmet  25184  cnmpopc  25304  xrhmeo  25322  oprpiece1res1  25327  htpycc  25356  pcoval1  25389  pcohtpylem  25395  pcoass  25400  pcorevlem  25402  ovolunlem1a  25872  ovolunlem1  25873  ovolicc2lem3  25895  ovolicc2lem4  25896  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  itg2const2  26117  itg2splitlem  26124  itg2split  26125  itg2cnlem1  26137  itg2cnlem2  26138  iblss2  26181  itgspliticc  26212  ditgpos  26231  limcres  26261  plyeq0lem  26584  plypf1  26586  coeeq2  26616  dvply1  26660  aareccl  26710  dvtaylp  26754  pserdvlem2  26812  lgamgulmlem4  27416  isppw  27498  vmappw  27500  muval1  27517  dchrelbasd  27623  dchr1  27641  dchrptlem2  27649  lgsdir2  27714  lgsne0  27719  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  2sqnn0  27822  rplogsumlem2  27869  dchrisum0flblem2  27893  dchrisum0fno1  27895  rplogsum  27911  pntrlog2bndlem5  27965  noinfbnd2  28145  expnnsval  28869  angmgmaddov2  29446  1loopgrvd2  30141  1hevtxdg1  30144  1egrvtxdg1  30147  crctcshwlkn0lem2  30457  crctcshlem4  30466  crctcsh  30470  clwlkclwwlklem2fv1  30643  eulercrct  30900  eucrct2eupth  30903  ccatws1f1o  33610  pmtridfv1  33755  pmtridfv2  33756  psgnfzto1stlem  33760  elrgspnlem2  33903  elrgspnlem3  33904  elrspunsn  34083  gsummoncoe1fzo  34232  psrnzr  34255  0mplrim  34257  mplasclco  34259  evlextv  34285  esplyind  34318  vieta  34323  fldextrspunlsp  34417  extdgfialglem2  34436  rtelextdg2lem  34469  2sqr3minply  34523  smattl  34541  smattr  34542  smatbl  34543  1smat1  34547  madjusmdetlem1  34570  madjusmdetlem2  34571  esumpinfval  34816  eulerpartlemgs2  35123  ballotlemsgt1  35254  ballotlemsel1i  35256  ballotlemsi  35258  signswmnd  35297  signsvtn  35324  gdlopcfv1  36013  gdlopcfv2  36014  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  fnlfvk30  36068  vonf1oonfo  36090  cvmliftlem10  36267  unblimceq0lem  37587  bj-rdg0gALT  38256  poimirlem1  38807  poimirlem2  38808  poimirlem5  38811  poimirlem6  38812  poimirlem12  38818  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  itg2addnc  38860  itg2gt0cn  38861  itgaddnclem2  38865  sdclem1  38943  cdlemefs27cl  41736  sticksstones9  43470  sticksstones10  43471  sticksstones12a  43473  unitscyglem1  43511  flcidc  44433  oe0suclim  44540  tfsconcatfv  44604  safesnsupfilb  44680  relexp01min  44974  relexpxpmin  44978  mnurnd  45528  ioondisj2  46778  ioondisj1  46779  lptioo1  46917  limsup10exlem  47055  icccncfext  47170  cncfiooicc  47177  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  ditgeq3d  47247  itgsubsticclem  47258  dirkerper  47379  dirkercncflem2  47387  fourierdlem40  47430  fourierdlem65  47454  fourierdlem74  47463  fourierdlem75  47464  fourierdlem78  47467  fourierdlem81  47470  fourierdlem97  47486  fourierdlem103  47492  fourierdlem104  47493  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  elaa2lem  47516  etransclem19  47536  etransclem22  47539  etransclem24  47541  etransclem35  47552  sge0pnfval  47656  isomenndlem  47813  hoicvrrex  47839  ovn0  47849  volicon0  47858  hsphoidmvle2  47868  hsphoidmvle  47869  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmvlelem2  47879  hoidmvlelem3  47880  hspmbllem1  47909  hspmbllem2  47910  volico2  47924  ovolval2lem  47926  ovnsubadd2lem  47928  ovolval4lem1  47932  vonioolem1  47963  vonioo  47965  vonicclem1  47966  vonicc  47968  tmachlem-agreeprod  48220  discsubc  50509  oppf1st2nd  50578  2oppf  50579  oppfval  50583  parhomidval  51077  parhomideq2  51080  parcoval2  51097  parmapcl  51102