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

Theorem ifbieq1d 4142
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 4141 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 4137 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2685 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-if 4120
This theorem is referenced by:  opeq1  4433  opeq2  4434  oieq1  8458  oieq2  8459  cantnflem1d  8623  cantnflem1  8624  iunfictbso  8975  ttukey2g  9376  bcval  13131  swrdval  13462  summolem2a  14490  zsum  14493  fsum  14495  sumss  14499  sumss2  14501  fsumcvg2  14502  fsumser  14505  isumless  14621  cbvprod  14689  prodmolem2a  14708  zprod  14711  fprod  14715  fprodntriv  14716  prodss  14721  rpnnen2lem1  14987  sadadd2lem  15228  sadadd2  15229  pcmpt  15643  pcmptdvds  15645  prmreclem2  15668  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  prmrec  15673  ramub1lem2  15778  ramcl  15780  prmop1  15789  prmonn2  15790  prmdvdsprmo  15793  fvprmselelfz  15795  fvprmselgcd1  15796  prmodvdslcmf  15798  prmgapprmo  15813  pmtrval  17917  pmtrdifellem3  17944  cyggenod2  18333  gsummpt1n0  18410  dmdprdsplitlem  18482  evlslem2  19560  coe1tmmul2fv  19696  coe1pwmulfv  19698  cyggic  19969  dmatmulcl  20354  scmatscmiddistr  20362  marrepval  20416  maducoeval  20493  maducoeval2  20494  minmar1val  20502  fclsval  21859  stdbdmetval  22366  stdbdxmet  22367  pcopt2  22869  cmetcaulem  23132  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  mbfposb  23465  i1fres  23517  i1fposd  23519  mbfi1fseqlem2  23528  mbfi1fseq  23533  mbfi1flimlem  23534  mbfi1flim  23535  itg2splitlem  23560  itg2cnlem1  23573  itg2cn  23575  isibl  23577  isibl2  23578  iblitg  23580  dfitg  23581  cbvitg  23587  itgeq2  23589  itgvallem  23596  iblneg  23614  itgneg  23615  itgss3  23626  itgcn  23654  deg1suble  23912  elply2  23997  dgrsub  24073  aareccl  24126  vmaval  24884  prmorcht  24949  pclogsum  24985  dchrelbasd  25009  dchrptlem2  25035  bposlem5  25058  lgsfval  25072  lgsdir  25102  lgsdilem2  25103  lgsdi  25104  lgsne0  25105  rplogsumlem2  25219  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  ballotlemsval  30698  ballotlemieq  30706  mrsubfval  31531  poimirlem1  33540  poimirlem5  33544  poimirlem6  33545  poimirlem12  33551  poimirlem22  33561  mblfinlem2  33577  itg2addnclem  33591  ftc1anclem5  33619  ftc1anclem6  33620  cdlemk40  36522  dvnprodlem1  40479  fourierdlem86  40727  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  isomennd  41066  hsphoif  41111  hsphoival  41114  sge0hsphoire  41124  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hspval  41144  hoidifhspval2  41150  hoidifhspval3  41154  hspmbllem2  41162  afveq12d  41534
  Copyright terms: Public domain W3C validator