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

Theorem ifbieq12d 3933
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 3928 . 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 3926 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2461 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   ifcif 3906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-un 3438  df-if 3907
This theorem is referenced by:  csbif  3956  tz7.44-2  7124  tz7.44-3  7125  boxcutc  7564  unxpdomlem1  7773  dfac12lem1  8562  dfac12r  8565  fin23lem12  8750  fin23lem33  8764  ttukeylem3  8930  ttukey2g  8935  xaddval  11505  seqf1olem2  12239  expval  12260  ccatfval  12695  ccatval1  12698  ccatval2  12699  relexpsucnnr  13056  ruclem1  14250  eucalgval2  14500  ressval  15128  gsumvalx  16457  gsumpropd  16459  gsumpropd2lem  16460  gsumress  16463  mulgval  16704  pmtrfv  17037  mvrfval  18572  xrsdsval  18940  marrepeval  19512  marepveval  19517  mdetunilem9  19569  madutpos  19591  madugsum  19592  minmar1eval  19598  symgmatr01lem  19602  symgmatr01  19603  gsummatr01lem3  19606  gsummatr01lem4  19607  gsummatr01  19608  ptcmplem3  20993  xrhmeo  21863  phtpycc  21908  pcovalg  21929  pcocn  21934  pcohtpylem  21936  pcoass  21941  pcorevlem  21943  ovolunlem1a  22323  ovolunlem1  22324  ioombl1  22389  mbfmax  22479  mbfpos  22481  mbfi1fseqlem2  22548  mbfi1fseq  22553  ditgeq1  22677  ditgeq2  22678  ig1pval  22995  cxpval  23471  lgamgulmlem4  23819  lgamgulmlem5  23820  musumsum  23981  muinv  23982  lgsval  24088  clwlkisclwwlklem2fv1  25352  gxval  25828  resvval  28426  psgnfzto1stlem  28449  smatrcl  28458  smatlem  28459  madjusmdetlem2  28490  madjusmdet  28493  ballotlemsv  29165  ballotlemsf1o  29169  plymulx0  29221  mrsubcv  29933  mrsubrn  29936  rdgprc0  30224  dfrdg2  30226  poimirlem2  31646  poimirlem23  31667  poimirlem24  31668  poimirlem27  31671  itg2addnclem3  31699  itgaddnclem2  31705  ftc1anclem5  31725  cdleme27b  33644  cdleme29b  33651  cdleme31sn  33656  cdleme31fv  33666  cdleme40v  33745  dihffval  34507  dihfval  34508  dihval  34509  aomclem8  35629  ifeq123d  37016  icccncfext  37341  dvnxpaek  37390  nnfoctbdjlem  37806
  Copyright terms: Public domain W3C validator