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

Theorem ifbieq12d 3587
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 3583 . 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 3581 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2315 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   ifcif 3565
This theorem is referenced by:  csbifg  3593  opeq1  3796  opeq2  3797  riotaeqdv  6305  riotabidv  6306  tz7.44-2  6420  tz7.44-3  6421  boxcutc  6859  unxpdomlem1  7067  oieq1  7227  oieq2  7228  cantnflem1d  7390  cantnflem1  7391  iunfictbso  7741  dfac12lem1  7769  dfac12r  7772  fin23lem12  7957  fin23lem33  7971  ttukeylem3  8138  ttukey2g  8143  xaddval  10550  seqf1olem2  11086  expval  11106  bcval  11317  ccatfval  11428  ccatval1  11431  ccatval2  11432  swrdval  11450  cbvsum  12168  summolem2a  12188  zsum  12191  fsum  12193  sumss  12197  sumss2  12199  fsumcvg2  12200  fsumser  12203  isumless  12304  rpnnen2lem1  12493  rpnnen  12505  ruclem1  12509  sadadd2lem  12650  sadadd2  12651  eucalgval2  12751  pcmpt  12940  pcmptdvds  12942  prmreclem2  12964  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  prmrec  12969  ramub1lem2  13074  ramcl  13076  ressval  13195  gsumvalx  14451  gsumpropd  14453  gsumress  14454  mulgval  14569  cyggenod2  15172  dmdprdsplitlem  15272  mvrfval  16165  evlslem2  16249  coe1tmmul2fv  16354  coe1pwmulfv  16356  xrsdsval  16415  cyggic  16526  fclsval  17703  ptcmplem3  17748  stdbdmetval  18060  stdbdxmet  18061  xrhmeo  18444  phtpycc  18489  pcovalg  18510  pcocn  18515  pcohtpylem  18517  pcopt2  18521  pcoass  18522  pcorevlem  18524  cmetcaulem  18714  ovolunlem1a  18855  ovolunlem1  18856  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1  18919  mbfmax  19004  mbfpos  19006  mbfposb  19008  i1fres  19060  i1fposd  19062  mbfi1fseqlem2  19071  mbfi1fseq  19076  mbfi1flimlem  19077  mbfi1flim  19078  itg2splitlem  19103  itg2cnlem1  19116  itg2cn  19118  isibl  19120  isibl2  19121  iblitg  19123  dfitg  19124  cbvitg  19130  itgeq2  19132  itgvallem  19139  iblneg  19157  itgneg  19158  itgss3  19169  itgcn  19197  ditgeq1  19198  ditgeq2  19199  deg1suble  19493  ig1pval  19558  elply2  19578  dgrsub  19653  aareccl  19706  cxpval  20011  vmaval  20351  prmorcht  20416  musumsum  20432  muinv  20433  pclogsum  20454  dchrelbasd  20478  dchrptlem2  20504  bposlem5  20527  lgsval  20539  lgsfval  20540  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  rplogsumlem2  20634  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  gxval  20925  ballotlemsval  23067  ballotlemsv  23068  ballotlemsf1o  23072  ballotlemieq  23075  gsumpropd2lem  23379  itgmeq123dTMP  23589  rdgprc0  24150  dfrdg2  24152  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  aomclem8  27159  pmtrval  27394  pmtrfv  27395  afveq12d  27996  cdleme27b  30557  cdleme29b  30564  cdleme31sn  30569  cdleme31fv  30579  cdleme40v  30658  cdlemk40  31106  dihffval  31420  dihfval  31421  dihval  31422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-if 3566
  Copyright terms: Public domain W3C validator