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

Theorem ifbieq1d 4086
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 4085 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3 ifbieq1d.2 . . 3 (𝜑𝐴 = 𝐵)
43ifeq1d 4081 . 2 (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
52, 4eqtrd 2660 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-v 3193  df-un 3565  df-if 4064
This theorem is referenced by:  opeq1  4375  opeq2  4376  oieq1  8362  oieq2  8363  cantnflem1d  8530  cantnflem1  8531  iunfictbso  8882  ttukey2g  9283  bcval  13028  swrdval  13350  summolem2a  14374  zsum  14377  fsum  14379  sumss  14383  sumss2  14385  fsumcvg2  14386  fsumser  14389  isumless  14497  cbvprod  14565  prodmolem2a  14584  zprod  14587  fprod  14591  fprodntriv  14592  prodss  14597  rpnnen2lem1  14863  sadadd2lem  15100  sadadd2  15101  pcmpt  15515  pcmptdvds  15517  prmreclem2  15540  prmreclem4  15542  prmreclem5  15543  prmreclem6  15544  prmrec  15545  ramub1lem2  15650  ramcl  15652  prmop1  15661  prmonn2  15662  prmdvdsprmo  15665  fvprmselelfz  15667  fvprmselgcd1  15668  prmodvdslcmf  15670  prmgapprmo  15685  pmtrval  17787  pmtrdifellem3  17814  cyggenod2  18203  gsummpt1n0  18280  dmdprdsplitlem  18352  evlslem2  19426  coe1tmmul2fv  19562  coe1pwmulfv  19564  cyggic  19835  dmatmulcl  20220  scmatscmiddistr  20228  marrepval  20282  maducoeval  20359  maducoeval2  20360  minmar1val  20368  fclsval  21717  stdbdmetval  22224  stdbdxmet  22225  pcopt2  22726  cmetcaulem  22989  ovolicc2lem3  23189  ovolicc2lem4  23190  ovolicc2lem5  23191  mbfposb  23321  i1fres  23373  i1fposd  23375  mbfi1fseqlem2  23384  mbfi1fseq  23389  mbfi1flimlem  23390  mbfi1flim  23391  itg2splitlem  23416  itg2cnlem1  23429  itg2cn  23431  isibl  23433  isibl2  23434  iblitg  23436  dfitg  23437  cbvitg  23443  itgeq2  23445  itgvallem  23452  iblneg  23470  itgneg  23471  itgss3  23482  itgcn  23510  deg1suble  23766  elply2  23851  dgrsub  23927  aareccl  23980  vmaval  24734  prmorcht  24799  pclogsum  24835  dchrelbasd  24859  dchrptlem2  24885  bposlem5  24908  lgsfval  24922  lgsdir  24952  lgsdilem2  24953  lgsdi  24954  lgsne0  24955  rplogsumlem2  25069  pntrlog2bndlem4  25164  pntrlog2bndlem5  25165  ballotlemsval  30343  ballotlemieq  30351  mrsubfval  31105  poimirlem1  33009  poimirlem5  33013  poimirlem6  33014  poimirlem12  33020  poimirlem22  33030  mblfinlem2  33046  itg2addnclem  33060  ftc1anclem5  33088  ftc1anclem6  33089  cdlemk40  35652  dvnprodlem1  39435  fourierdlem86  39684  fourierdlem97  39695  fourierdlem103  39701  fourierdlem104  39702  fourierdlem112  39710  isomennd  40020  hsphoif  40065  hsphoival  40068  sge0hsphoire  40078  hoidmv1lelem2  40081  hoidmv1lelem3  40082  hoidmv1le  40083  hoidmvlelem1  40084  hoidmvlelem2  40085  hoidmvlelem3  40086  hoidmvlelem4  40087  hoidmvlelem5  40088  hspval  40098  hoidifhspval2  40104  hoidifhspval3  40108  hspmbllem2  40116  afveq12d  40485
  Copyright terms: Public domain W3C validator