MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbieq12d Unicode version

Theorem ifbieq12d 3588
Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
ifbieq12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
ifbieq12d.2  |-  ( ph  ->  A  =  C )
ifbieq12d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
ifbieq12d  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)

Proof of Theorem ifbieq12d
StepHypRef Expression
1 ifbieq12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ifbid 3584 . 2  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
3 ifbieq12d.2 . . 3  |-  ( ph  ->  A  =  C )
4 ifbieq12d.3 . . 3  |-  ( ph  ->  B  =  D )
53, 4ifeq12d 3582 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2316 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1624   ifcif 3566
This theorem is referenced by:  csbifg  3594  opeq1  3797  opeq2  3798  riotaeqdv  6300  riotabidv  6301  tz7.44-2  6415  tz7.44-3  6416  boxcutc  6854  unxpdomlem1  7062  oieq1  7222  oieq2  7223  cantnflem1d  7385  cantnflem1  7386  iunfictbso  7736  dfac12lem1  7764  dfac12r  7767  fin23lem12  7952  fin23lem33  7966  ttukeylem3  8133  ttukey2g  8138  xaddval  10544  seqf1olem2  11080  expval  11100  bcval  11311  ccatfval  11422  ccatval1  11425  ccatval2  11426  swrdval  11444  cbvsum  12162  summolem2a  12182  zsum  12185  fsum  12187  sumss  12191  sumss2  12193  fsumcvg2  12194  fsumser  12197  isumless  12298  rpnnen2lem1  12487  rpnnen  12499  ruclem1  12503  sadadd2lem  12644  sadadd2  12645  eucalgval2  12745  pcmpt  12934  pcmptdvds  12936  prmreclem2  12958  prmreclem4  12960  prmreclem5  12961  prmreclem6  12962  prmrec  12963  ramub1lem2  13068  ramcl  13070  ressval  13189  gsumvalx  14445  gsumpropd  14447  gsumress  14448  mulgval  14563  cyggenod2  15166  dmdprdsplitlem  15266  mvrfval  16159  evlslem2  16243  coe1tmmul2fv  16348  coe1pwmulfv  16350  xrsdsval  16409  cyggic  16520  fclsval  17697  ptcmplem3  17742  stdbdmetval  18054  stdbdxmet  18055  xrhmeo  18438  phtpycc  18483  pcovalg  18504  pcocn  18509  pcohtpylem  18511  pcopt2  18515  pcoass  18516  pcorevlem  18518  cmetcaulem  18708  ovolunlem1a  18849  ovolunlem1  18850  ovolicc2lem3  18872  ovolicc2lem4  18873  ovolicc2lem5  18874  ioombl1  18913  mbfmax  18998  mbfpos  19000  mbfposb  19002  i1fres  19054  i1fposd  19056  mbfi1fseqlem2  19065  mbfi1fseq  19070  mbfi1flimlem  19071  mbfi1flim  19072  itg2splitlem  19097  itg2cnlem1  19110  itg2cn  19112  isibl  19114  isibl2  19115  iblitg  19117  dfitg  19118  cbvitg  19124  itgeq2  19126  itgvallem  19133  iblneg  19151  itgneg  19152  itgss3  19163  itgcn  19191  ditgeq1  19192  ditgeq2  19193  deg1suble  19487  ig1pval  19552  elply2  19572  dgrsub  19647  aareccl  19700  cxpval  20005  vmaval  20345  prmorcht  20410  musumsum  20426  muinv  20427  pclogsum  20448  dchrelbasd  20472  dchrptlem2  20498  bposlem5  20521  lgsval  20533  lgsfval  20534  lgsdir  20563  lgsdilem2  20564  lgsdi  20565  lgsne0  20566  rplogsumlem2  20628  pntrlog2bndlem4  20723  pntrlog2bndlem5  20724  gxval  20917  ballotlemsval  23060  ballotlemsv  23061  ballotlemsf1o  23065  ballotlemieq  23068  rdgprc0  23551  dfrdg2  23553  lineval222  25478  lineval3a  25482  sgplpte21  25531  sgplpte22  25537  isray2  25552  isray  25553  aomclem8  26558  pmtrval  26793  pmtrfv  26794  afveq12d  27373  cdleme27b  29824  cdleme29b  29831  cdleme31sn  29836  cdleme31fv  29846  cdleme40v  29925  cdlemk40  30373  dihffval  30687  dihfval  30688  dihval  30689
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-un 3158  df-if 3567
  Copyright terms: Public domain W3C validator