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

Theorem ifbieq12d 3907
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 3902 . 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 3900 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2484 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1443   ifcif 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-un 3408  df-if 3881
This theorem is referenced by:  csbif  3930  tz7.44-2  7122  tz7.44-3  7123  boxcutc  7562  unxpdomlem1  7773  dfac12lem1  8570  dfac12r  8573  fin23lem12  8758  fin23lem33  8772  ttukeylem3  8938  ttukey2g  8943  xaddval  11513  seqf1olem2  12250  expval  12271  ccatfval  12716  ccatval1  12719  ccatval2  12720  relexpsucnnr  13081  ruclem1  14276  eucalgval2  14533  ressval  15169  gsumvalx  16506  gsumpropd  16508  gsumpropd2lem  16509  gsumress  16512  mulgval  16753  pmtrfv  17086  mvrfval  18637  xrsdsval  19005  marrepeval  19581  marepveval  19586  mdetunilem9  19638  madutpos  19660  madugsum  19661  minmar1eval  19667  symgmatr01lem  19671  symgmatr01  19672  gsummatr01lem3  19675  gsummatr01lem4  19676  gsummatr01  19677  ptcmplem3  21062  xrhmeo  21967  phtpycc  22015  pcovalg  22036  pcocn  22041  pcohtpylem  22043  pcoass  22048  pcorevlem  22050  ovolunlem1a  22442  ovolunlem1  22443  ioombl1  22508  mbfmax  22598  mbfpos  22600  mbfi1fseqlem2  22667  mbfi1fseq  22672  ditgeq1  22796  ditgeq2  22797  ig1pval  23117  ig1pvalOLD  23123  cxpval  23602  lgamgulmlem4  23950  lgamgulmlem5  23951  musumsum  24114  muinv  24115  lgsval  24221  clwlkisclwwlklem2fv1  25503  gxval  25979  resvval  28583  psgnfzto1stlem  28606  smatrcl  28615  smatlem  28616  madjusmdetlem2  28647  madjusmdet  28650  ballotlemsv  29335  ballotlemsf1o  29339  ballotlemsvOLD  29373  ballotlemsf1oOLD  29377  plymulx0  29429  mrsubcv  30141  mrsubrn  30144  rdgprc0  30433  dfrdg2  30435  csbopg2  31718  csbrdgg  31723  csbfinxpg  31773  finxpreclem3  31778  poimirlem2  31935  poimirlem23  31956  poimirlem24  31957  poimirlem27  31960  itg2addnclem3  31988  itgaddnclem2  31994  ftc1anclem5  32014  cdleme27b  33929  cdleme29b  33936  cdleme31sn  33941  cdleme31fv  33951  cdleme40v  34030  dihffval  34792  dihfval  34793  dihval  34794  aomclem8  35913  ifeq123d  37366  icccncfext  37759  dvnxpaek  37811  nnfoctbdjlem  38287  hsphoival  38395  sge0hsphoire  38405  hoidmvlelem1  38411  hoidmvlelem2  38412  hoidmvlelem3  38413  hoidmvlelem4  38414  hoidmvlelem5  38415  hoidifhspval3  38435  hspmbllem2  38443  vtxval  39091  iedgval  39092
  Copyright terms: Public domain W3C validator