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

Theorem ifbieq1d 3962
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 3961 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 3957 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2548 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-un 3449  df-if 3940
This theorem is referenced by:  opeq1  4238  opeq2  4239  oieq1  8175  oieq2  8176  cantnflem1d  8343  cantnflem1  8344  iunfictbso  8695  ttukey2g  9096  bcval  12820  swrdval  13126  summolem2a  14160  zsum  14163  fsum  14165  sumss  14169  sumss2  14171  fsumcvg2  14172  fsumser  14175  isumless  14283  cbvprod  14351  prodmolem2a  14370  zprod  14373  fprod  14377  fprodntriv  14378  prodss  14383  rpnnen2lem1  14649  sadadd2lem  14890  sadadd2  14891  pcmpt  15316  pcmptdvds  15318  prmreclem2  15341  prmreclem4  15343  prmreclem5  15344  prmreclem6  15345  prmrec  15346  ramub1lem2  15451  ramcl  15453  prmop1  15462  prmonn2  15463  prmdvdsprmo  15466  fvprmselelfz  15468  fvprmselgcd1  15469  prmodvdslcmf  15471  prmgapprmo  15486  pmtrval  17584  pmtrdifellem3  17611  cyggenod2  18015  gsummpt1n0  18092  dmdprdsplitlem  18164  evlslem2  19235  coe1tmmul2fv  19371  coe1pwmulfv  19373  cyggic  19644  dmatmulcl  20026  scmatscmiddistr  20034  marrepval  20088  maducoeval  20165  maducoeval2  20166  minmar1val  20174  fclsval  21523  stdbdmetval  22029  stdbdxmet  22030  pcopt2  22555  cmetcaulem  22759  ovolicc2lem3  22970  ovolicc2lem4  22971  ovolicc2lem5  22972  mbfposb  23102  i1fres  23154  i1fposd  23156  mbfi1fseqlem2  23165  mbfi1fseq  23170  mbfi1flimlem  23171  mbfi1flim  23172  itg2splitlem  23197  itg2cnlem1  23210  itg2cn  23212  isibl  23214  isibl2  23215  iblitg  23217  dfitg  23218  cbvitg  23224  itgeq2  23226  itgvallem  23233  iblneg  23251  itgneg  23252  itgss3  23263  itgcn  23291  deg1suble  23547  elply2  23641  dgrsub  23717  aareccl  23773  vmaval  24529  prmorcht  24594  pclogsum  24630  dchrelbasd  24654  dchrptlem2  24680  bposlem5  24703  lgsfval  24717  lgsdir  24747  lgsdilem2  24748  lgsdi  24749  lgsne0  24750  rplogsumlem2  24864  pntrlog2bndlem4  24959  pntrlog2bndlem5  24960  ballotlemsval  29705  ballotlemieq  29713  ballotlemsvalOLD  29743  ballotlemieqOLD  29751  mrsubfval  30505  poimirlem1  32455  poimirlem5  32459  poimirlem6  32460  poimirlem12  32466  poimirlem22  32476  mblfinlem2  32492  itg2addnclem  32506  ftc1anclem5  32534  ftc1anclem6  32535  cdlemk40  35098  dvnprodlem1  38726  fourierdlem86  38977  fourierdlem97  38988  fourierdlem103  38994  fourierdlem104  38995  fourierdlem112  39003  isomennd  39315  hsphoif  39360  hsphoival  39363  sge0hsphoire  39373  hoidmv1lelem2  39376  hoidmv1lelem3  39377  hoidmv1le  39378  hoidmvlelem1  39379  hoidmvlelem2  39380  hoidmvlelem3  39381  hoidmvlelem4  39382  hoidmvlelem5  39383  hspval  39393  hoidifhspval2  39399  hoidifhspval3  39403  hspmbllem2  39411  afveq12d  39757
  Copyright terms: Public domain W3C validator