MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbieq1d Structured version   Visualization version   GIF version

Theorem ifbieq1d 4058
Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)
Hypotheses
Ref Expression
ifbieq1d.1 (𝜑 → (𝜓𝜒))
ifbieq1d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifbieq1d (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Proof of Theorem ifbieq1d
StepHypRef Expression
1 ifbieq1d.1 . . 3 (𝜑 → (𝜓𝜒))
21ifbid 4057 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 4053 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2643 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-un 3544  df-if 4036
This theorem is referenced by:  opeq1  4334  opeq2  4335  oieq1  8277  oieq2  8278  cantnflem1d  8445  cantnflem1  8446  iunfictbso  8797  ttukey2g  9198  bcval  12908  swrdval  13215  summolem2a  14239  zsum  14242  fsum  14244  sumss  14248  sumss2  14250  fsumcvg2  14251  fsumser  14254  isumless  14362  cbvprod  14430  prodmolem2a  14449  zprod  14452  fprod  14456  fprodntriv  14457  prodss  14462  rpnnen2lem1  14728  sadadd2lem  14965  sadadd2  14966  pcmpt  15380  pcmptdvds  15382  prmreclem2  15405  prmreclem4  15407  prmreclem5  15408  prmreclem6  15409  prmrec  15410  ramub1lem2  15515  ramcl  15517  prmop1  15526  prmonn2  15527  prmdvdsprmo  15530  fvprmselelfz  15532  fvprmselgcd1  15533  prmodvdslcmf  15535  prmgapprmo  15550  pmtrval  17640  pmtrdifellem3  17667  cyggenod2  18056  gsummpt1n0  18133  dmdprdsplitlem  18205  evlslem2  19279  coe1tmmul2fv  19415  coe1pwmulfv  19417  cyggic  19685  dmatmulcl  20067  scmatscmiddistr  20075  marrepval  20129  maducoeval  20206  maducoeval2  20207  minmar1val  20215  fclsval  21564  stdbdmetval  22070  stdbdxmet  22071  pcopt2  22562  cmetcaulem  22812  ovolicc2lem3  23011  ovolicc2lem4  23012  ovolicc2lem5  23013  mbfposb  23143  i1fres  23195  i1fposd  23197  mbfi1fseqlem2  23206  mbfi1fseq  23211  mbfi1flimlem  23212  mbfi1flim  23213  itg2splitlem  23238  itg2cnlem1  23251  itg2cn  23253  isibl  23255  isibl2  23256  iblitg  23258  dfitg  23259  cbvitg  23265  itgeq2  23267  itgvallem  23274  iblneg  23292  itgneg  23293  itgss3  23304  itgcn  23332  deg1suble  23588  elply2  23673  dgrsub  23749  aareccl  23802  vmaval  24556  prmorcht  24621  pclogsum  24657  dchrelbasd  24681  dchrptlem2  24707  bposlem5  24730  lgsfval  24744  lgsdir  24774  lgsdilem2  24775  lgsdi  24776  lgsne0  24777  rplogsumlem2  24891  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  ballotlemsval  29703  ballotlemieq  29711  mrsubfval  30465  poimirlem1  32383  poimirlem5  32387  poimirlem6  32388  poimirlem12  32394  poimirlem22  32404  mblfinlem2  32420  itg2addnclem  32434  ftc1anclem5  32462  ftc1anclem6  32463  cdlemk40  35026  dvnprodlem1  38640  fourierdlem86  38889  fourierdlem97  38900  fourierdlem103  38906  fourierdlem104  38907  fourierdlem112  38915  isomennd  39225  hsphoif  39270  hsphoival  39273  sge0hsphoire  39283  hoidmv1lelem2  39286  hoidmv1lelem3  39287  hoidmv1le  39288  hoidmvlelem1  39289  hoidmvlelem2  39290  hoidmvlelem3  39291  hoidmvlelem4  39292  hoidmvlelem5  39293  hspval  39303  hoidifhspval2  39309  hoidifhspval3  39313  hspmbllem2  39321  afveq12d  39667
  Copyright terms: Public domain W3C validator