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

Theorem ifbieq1d 3931
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 3930 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 3926 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2539 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191   = wceq 1468  ifcif 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rab 2800  df-v 3068  df-un 3431  df-if 3909
This theorem is referenced by:  opeq1  4196  opeq2  4197  oieq1  8110  oieq2  8111  cantnflem1d  8278  cantnflem1  8279  iunfictbso  8630  ttukey2g  9031  bcval  12603  swrdval  12907  summolem2a  13941  zsum  13944  fsum  13946  sumss  13950  sumss2  13952  fsumcvg2  13953  fsumser  13956  isumless  14063  cbvprod  14129  prodmolem2a  14148  zprod  14151  fprod  14155  fprodntriv  14156  prodss  14161  rpnnen2lem1  14427  rpnnen  14439  sadadd2lem  14595  sadadd2  14596  pcmpt  14999  pcmptdvds  15001  prmreclem2  15023  prmreclem4  15025  prmreclem5  15026  prmreclem6  15027  prmrec  15028  ramub1lem2  15147  ramcl  15149  prmop1  15158  prmonn2  15159  prmdvdsprmo  15162  fvprmselelfz  15164  fvprmselgcd1  15165  prmodvdslcmf  15167  prmormapnnOLD  15176  prmdvdsprmorOLD  15177  prmorlefacOLD  15180  prmgapprmo  15195  pmtrval  17253  pmtrdifellem3  17280  cyggenod2  17681  gsummpt1n0  17758  dmdprdsplitlem  17830  evlslem2  18894  coe1tmmul2fv  19030  coe1pwmulfv  19032  cyggic  19301  dmatmulcl  19683  scmatscmiddistr  19691  marrepval  19745  maducoeval  19822  maducoeval2  19823  minmar1val  19831  fclsval  21181  stdbdmetval  21687  stdbdxmet  21688  pcopt2  22213  cmetcaulem  22417  ovolicc2lem3  22631  ovolicc2lem4OLD  22632  ovolicc2lem4  22633  ovolicc2lem5  22634  mbfposb  22770  i1fres  22824  i1fposd  22826  mbfi1fseqlem2  22835  mbfi1fseq  22840  mbfi1flimlem  22841  mbfi1flim  22842  itg2splitlem  22867  itg2cnlem1  22880  itg2cn  22882  isibl  22884  isibl2  22885  iblitg  22887  dfitg  22888  cbvitg  22894  itgeq2  22896  itgvallem  22903  iblneg  22921  itgneg  22922  itgss3  22933  itgcn  22961  deg1suble  23217  elply2  23311  dgrsub  23387  aareccl  23443  vmaval  24201  prmorcht  24266  pclogsum  24304  dchrelbasd  24328  dchrptlem2  24354  bposlem5  24377  lgsfval  24390  lgsdir  24419  lgsdilem2  24420  lgsdi  24421  lgsne0  24422  rplogsumlem2  24484  pntrlog2bndlem4  24579  pntrlog2bndlem5  24580  ballotlemsval  29495  ballotlemieq  29503  ballotlemsvalOLD  29533  ballotlemieqOLD  29541  mrsubfval  30298  poimirlem1  32179  poimirlem5  32183  poimirlem6  32184  poimirlem12  32190  poimirlem22  32200  mblfinlem2  32216  itg2addnclem  32231  ftc1anclem5  32259  ftc1anclem6  32260  cdlemk40  34724  dvnprodlem1  38240  fourierdlem86  38492  fourierdlem97  38503  fourierdlem103  38509  fourierdlem104  38510  fourierdlem112  38518  isomennd  38816  hsphoif  38861  hsphoival  38864  sge0hsphoire  38874  hoidmv1lelem2  38877  hoidmv1lelem3  38878  hoidmv1le  38879  hoidmvlelem1  38880  hoidmvlelem2  38881  hoidmvlelem3  38882  hoidmvlelem4  38883  hoidmvlelem5  38884  hspval  38894  hoidifhspval2  38900  hoidifhspval3  38904  hspmbllem2  38912  afveq12d  39155
  Copyright terms: Public domain W3C validator