Theorem iftrued 4094

Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iftrued.1	|- ( ph -> ch )

Assertion

Ref	Expression
iftrued	|- ( ph -> if ( ch , A , B ) = A )

Proof of Theorem iftrued

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 |- ( ph -> ch )
2		iftrue 4092	. 2 |- ( ch -> if ( ch , A , B ) = A )
3	1, 2	syl 17	1 |- ( ph -> if ( ch , A , B ) = A )

Syntax hints:   -> wi 4   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  mpt2snif  6754  tz7.44-3  7504  iunfictbso  8937  ttukeylem7  9337  max0sub  12027  ifle  12028  xmulneg1  12099  xmulpnf1  12104  expnnval  12863  swrdval2  13420  swrdlend  13431  swrd0  13434  swrdccatid  13497  relexp0g  13762  max0add  14050  summolem2a  14446  prodmolem2a  14664  ef0lem  14809  rpnnen2lem3  14945  rpnnen2lem9  14951  iserodd  15540  pcmpt  15596  pcmpt2  15597  prmdvdsprmo  15746  setcepi  16738  gsumval2a  17279  mgm2nsgrplem3  17407  mulgnn  17547  pmtrprfv  17873  pmtrprfval  17907  psgnunilem1  17913  dfod2  17981  oddvds2  17983  cyggenod  18286  mplcoe1  19465  mplcoe5  19468  coe1tm  19643  coe1tmmul2fv  19648  coe1pwmulfv  19650  coe1sclmul  19652  coe1sclmul2  19654  m1detdiag  20403  mdetunilem9  20426  maducoeval2  20446  symgmatr01lem  20459  pmatcollpw3fi1lem1  20591  chpmat1dlem  20640  chfacffsupp  20661  chfacfscmul0  20663  chfacfpmmul0  20667  2ndcdisj  21259  dscmet  22377  xrsxmet  22612  cnmpt2pc  22727  xrhmeo  22745  oprpiece1res1  22750  htpycc  22779  pcoval1  22813  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  ovolunlem1a  23264  ovolunlem1  23265  ovolicc2lem3  23287  ovolicc2lem4  23288  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2const2  23508  itg2splitlem  23515  itg2split  23516  itg2cnlem1  23528  itg2cnlem2  23529  iblss2  23572  itgspliticc  23603  ditgpos  23620  limcres  23650  plyeq0lem  23966  plypf1  23968  coeeq2  23998  dvply1  24039  aareccl  24081  dvtaylp  24124  pserdvlem2  24182  lgamgulmlem4  24758  isppw  24840  vmappw  24842  muval1  24859  dchrelbasd  24964  dchr1  24982  dchrptlem2  24990  lgsdir2  25055  lgsne0  25060  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  rplogsumlem2  25174  dchrisum0flblem2  25198  dchrisum0fno1  25200  rplogsum  25216  pntrlog2bndlem5  25270  1loopgrvd2  26399  1hevtxdg1  26402  1egrvtxdg1  26405  crctcshwlkn0lem2  26703  crctcshlem4  26712  crctcsh  26716  clwlkclwwlklem2fv1  26896  eulercrct  27102  eucrct2eupth  27105  partfun  29475  ofldchr  29814  psgnfzto1stlem  29850  pmtridfv1  29857  pmtridfv2  29858  smattl  29864  smattr  29865  smatbl  29866  1smat1  29870  madjusmdetlem1  29893  madjusmdetlem2  29894  esumpinfval  30135  eulerpartlemgs2  30442  ballotlemsgt1  30572  ballotlemsel1i  30574  ballotlemsi  30576  signswmnd  30634  signsvtn  30661  cvmliftlem10  31276  unblimceq0lem  32497  poimirlem1  33410  poimirlem2  33411  poimirlem5  33414  poimirlem6  33415  poimirlem12  33421  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  itg2addnc  33464  itg2gt0cn  33465  itgaddnclem2  33469  sdclem1  33539  cdlemefs27cl  35701  flcidc  37744  relexp01min  38005  relexpxpmin  38009  ioondisj2  39714  ioondisj1  39715  lptioo1  39864  limsup10exlem  40004  icccncfext  40100  cncfiooicc  40107  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnxpaek  40157  ditgeq3d  40180  itgsubsticclem  40191  dirkerper  40313  dirkercncflem2  40321  fourierdlem40  40364  fourierdlem65  40388  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem81  40404  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem19  40470  etransclem22  40473  etransclem24  40475  etransclem35  40486  sge0pnfval  40590  isomenndlem  40744  hoicvrrex  40770  ovn0  40780  volicon0  40789  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmvlelem2  40810  hoidmvlelem3  40811  hspmbllem1  40840  hspmbllem2  40841  volico2  40855  ovolval2lem  40857  ovnsubadd2lem  40859  ovolval4lem1  40863  vonioolem1  40894  vonioo  40896  vonicclem1  40897  vonicc  40899