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

Theorem bibi12d 321
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)
Hypotheses
Ref Expression
imbi12d.1
imbi12d.2
Assertion
Ref Expression
bibi12d

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3
21bibi1d 319 . 2
3 imbi12d.2 . . 3
43bibi2d 318 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  bi2bian9  875  xorbi12d  1377  sb8eu  2318  cleqh  2572  cleqhOLD  2573  abbiOLD  2589  cleqfOLD  2647  vtoclb  3164  vtoclbg  3168  ceqsexg  3231  elabgf  3244  reu6  3288  ru  3326  sbcbig  3374  unineq  3747  sbcnestgf  3839  preq12bg  4209  prel12g  4210  axrep1  4564  axrep4  4567  nalset  4589  opthg  4727  opelopabsb  4762  isso2i  4837  opeliunxp2  5146  resieq  5289  elimasng  5368  cbviota  5561  iota2df  5580  fnbrfvb  5913  fvelimab  5929  fvopab5  5979  fmptco  6064  fsng  6070  fressnfv  6085  isorel  6222  isocnv  6226  isocnv3  6228  isotr  6232  ovg  6441  caovcang  6476  caovordg  6482  caovord3d  6485  caovord  6486  orduninsuc  6678  brtpos  6983  dftpos4  6993  omopth  7326  ecopovsym  7432  xpf1o  7699  nneneq  7720  r1pwOLD  8285  karden  8334  infxpenlem  8412  aceq0  8520  cflim2  8664  zfac  8861  ttukeylem1  8910  axextnd  8987  axrepndlem1  8988  axrepndlem2  8989  axrepnd  8990  axacndlem5  9010  zfcndrep  9013  zfcndac  9018  winalim  9094  gruina  9217  ltrnq  9378  ltsosr  9492  ltasr  9498  axpre-lttri  9563  axpre-ltadd  9565  nn0sub  10871  zextle  10961  zextlt  10962  xlesubadd  11484  sqeqor  12282  nn0opth2  12352  rexfiuz  13180  climshft  13399  rpnnen2lem10  13957  dvdsext  14037  sadcadd  14108  dvdssq  14198  isprm2lem  14224  rpexp  14261  pcdvdsb  14392  imasleval  14938  isacs2  15050  acsfiel  15051  funcres2b  15266  pospropd  15764  isnsg  16230  nsgbi  16232  elnmz  16240  nmzbi  16241  oddvdsnn0  16568  odeq  16574  odmulg  16578  isslw  16628  slwispgp  16631  gsumval3OLD  16908  gsumval3lem2  16910  gsumcom2  17003  abveq0  17475  cnt0  19847  kqfvima  20231  kqt0lem  20237  isr0  20238  r0cld  20239  regr1lem2  20241  nrmr0reg  20250  isfildlem  20358  cnextfvval  20565  xmeteq0  20841  imasf1oxmet  20878  comet  21016  dscmet  21093  nrmmetd  21095  tngngp  21168  mbfsup  22071  mbfinf  22072  degltlem1  22472  logltb  22984  cxple2  23078  rlimcnp  23295  rlimcnp2  23296  isppw2  23389  sqf11  23413  f1otrgitv  24173  isrgrac  24934  eupath2lem3  24979  nmlno0i  25709  nmlno0  25710  blocn  25722  ubth  25789  hvsubeq0  25985  hvaddcan  25987  hvsubadd  25994  normsub0  26053  hlim2  26109  pjoc1  26352  pjoc2  26357  chne0  26412  chsscon3  26418  chlejb1  26430  chnle  26432  h1de2ci  26474  elspansn  26484  elspansn2  26485  cmbr3  26526  cmcm  26532  cmcm3  26533  pjch1  26588  pjch  26612  pj11  26632  pjnel  26644  eigorth  26757  elnlfn  26847  nmlnop0  26917  lnopeq  26928  lnopcon  26954  lnfncon  26975  pjdifnormi  27086  chrelat2  27289  cvexch  27293  mdsym  27331  fmptcof2  27502  signswch  28518  cvmlift2lem12  28759  cvmlift2lem13  28760  abs2sqle  29046  abs2sqlt  29047  dfpo2  29184  axextdist  29232  brimageg  29577  brdomaing  29585  brrangeg  29586  elhf2  29832  onsuct0  29906  nn0prpwlem  30140  nn0prpw  30141  prdsbnd2  30291  isdrngo1  30359  zindbi  30882  divalgmodcl  30929  wepwsolem  30987  aomclem8  31007  2sbc6g  31322  2sbc5g  31323  fourierdlem31  31920  fourierdlem42  31931  fourierdlem54  31943  bj-cleqh  34358  bj-abbi  34361  bj-axrep1  34374  bj-axrep4  34377  bj-nalset  34380  bj-sbceqgALT  34469  bj-ru0  34500  lsatcmp  34728  llnexchb2  35593  lautset  35806  lautle  35808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator