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

Theorem ifbieq12d 3971
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 3966 . 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 3964 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2498 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395   ifcif 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-un 3476  df-if 3945
This theorem is referenced by:  csbif  3994  csbifgOLD  3995  tz7.44-2  7091  tz7.44-3  7092  boxcutc  7531  unxpdomlem1  7743  dfac12lem1  8540  dfac12r  8543  fin23lem12  8728  fin23lem33  8742  ttukeylem3  8908  ttukey2g  8913  xaddval  11447  seqf1olem2  12149  expval  12170  ccatfval  12600  ccatval1  12603  ccatval2  12604  ruclem1  13975  eucalgval2  14221  ressval  14697  gsumvalx  16023  gsumpropd  16025  gsumpropd2lem  16026  gsumress  16029  mulgval  16270  pmtrfv  16603  mvrfval  18202  xrsdsval  18588  marrepeval  19191  marepveval  19196  mdetunilem9  19248  madutpos  19270  madugsum  19271  minmar1eval  19277  symgmatr01lem  19281  symgmatr01  19282  gsummatr01lem3  19285  gsummatr01lem4  19286  gsummatr01  19287  ptcmplem3  20679  xrhmeo  21571  phtpycc  21616  pcovalg  21637  pcocn  21642  pcohtpylem  21644  pcoass  21649  pcorevlem  21651  ovolunlem1a  22032  ovolunlem1  22033  ioombl1  22097  mbfmax  22181  mbfpos  22183  mbfi1fseqlem2  22248  mbfi1fseq  22253  ditgeq1  22377  ditgeq2  22378  ig1pval  22698  cxpval  23170  musumsum  23593  muinv  23594  lgsval  23700  clwlkisclwwlklem2fv1  24908  gxval  25386  resvval  27970  ballotlemsv  28623  ballotlemsf1o  28627  plymulx0  28679  lgamgulmlem4  28749  lgamgulmlem5  28750  mrsubcv  29045  mrsubrn  29048  rdgprc0  29400  dfrdg2  29402  itg2addnclem3  30230  itgaddnclem2  30236  ftc1anclem5  30256  aomclem8  31169  ifeq123d  31593  icccncfext  31851  dvnxpaek  31900  cdleme27b  36195  cdleme29b  36202  cdleme31sn  36207  cdleme31fv  36217  cdleme40v  36296  dihffval  37058  dihfval  37059  dihval  37060
  Copyright terms: Public domain W3C validator