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

Theorem ifbieq1d 4451
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 4450 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 4446 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2836 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  ifcif 4428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-un 3889  df-if 4429
This theorem is referenced by:  opeq1OLD  4767  opeq2OLD  4769  oieq1  8964  oieq2  8965  cantnflem1d  9139  cantnflem1  9140  iunfictbso  9529  ttukey2g  9931  bcval  13664  swrdval  14000  summolem2a  15068  zsum  15071  fsum  15073  sumss  15077  sumss2  15079  fsumcvg2  15080  fsumser  15083  isumless  15196  cbvprod  15265  prodmolem2a  15284  zprod  15287  fprod  15291  fprodntriv  15292  prodss  15297  rpnnen2lem1  15563  sadadd2lem  15802  sadadd2  15803  pcmpt  16222  pcmptdvds  16224  prmreclem2  16247  prmreclem4  16249  prmreclem5  16250  prmreclem6  16251  prmrec  16252  ramub1lem2  16357  ramcl  16359  prmop1  16368  prmonn2  16369  prmdvdsprmo  16372  fvprmselelfz  16374  fvprmselgcd1  16375  prmodvdslcmf  16377  prmgapprmo  16392  smndex2dlinvh  18078  pmtrval  18575  pmtrdifellem3  18602  cyggenod2  19001  gsummpt1n0  19082  dmdprdsplitlem  19156  cycsubggenodd  19228  cyggic  20268  evlslem2  20755  coe1tmmul2fv  20911  coe1pwmulfv  20913  dmatmulcl  21109  scmatscmiddistr  21117  marrepval  21171  maducoeval  21248  maducoeval2  21249  minmar1val  21257  fclsval  22617  stdbdmetval  23125  stdbdxmet  23126  pcopt2  23632  cmetcaulem  23896  ovolicc2lem3  24127  ovolicc2lem4  24128  ovolicc2lem5  24129  mbfposb  24261  i1fres  24313  i1fposd  24315  mbfi1fseqlem2  24324  mbfi1fseq  24329  mbfi1flimlem  24330  mbfi1flim  24331  itg2splitlem  24356  itg2cnlem1  24369  itg2cn  24371  isibl  24373  isibl2  24374  iblitg  24376  dfitg  24377  cbvitg  24383  itgeq2  24385  itgvallem  24392  iblneg  24410  itgneg  24411  itgss3  24422  itgcn  24452  deg1suble  24712  elply2  24797  dgrsub  24873  aareccl  24926  vmaval  25702  prmorcht  25767  pclogsum  25803  dchrelbasd  25827  dchrptlem2  25853  bposlem5  25876  lgsfval  25890  lgsdir  25920  lgsdilem2  25921  lgsdi  25922  lgsne0  25923  rplogsumlem2  26073  pntrlog2bndlem4  26168  pntrlog2bndlem5  26169  ballotlemsval  31880  ballotlemieq  31888  mrsubfval  32869  poimirlem1  35057  poimirlem5  35061  poimirlem6  35062  poimirlem12  35068  poimirlem22  35078  mblfinlem2  35094  itg2addnclem  35107  ftc1anclem5  35133  ftc1anclem6  35134  cdlemk40  38212  fsuppind  39449  dvnprodlem1  42581  fourierdlem86  42827  fourierdlem97  42838  fourierdlem103  42844  fourierdlem104  42845  fourierdlem112  42853  isomennd  43163  hsphoif  43208  hsphoival  43211  sge0hsphoire  43221  hoidmv1lelem2  43224  hoidmv1lelem3  43225  hoidmv1le  43226  hoidmvlelem1  43227  hoidmvlelem2  43228  hoidmvlelem3  43229  hoidmvlelem4  43230  hoidmvlelem5  43231  hspval  43241  hoidifhspval2  43247  hoidifhspval3  43251  hspmbllem2  43259  afveq12d  43682
  Copyright terms: Public domain W3C validator