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

Theorem bibi12d 347
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 345 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 344 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 280 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  bi2bian9  637  xorbi12d  1509  norass  1524  sbbib  2373  sb8eulem  2680  abbi  2888  cleqh  2936  cleqf  3010  vtoclb  3565  vtoclbg  3569  ceqsexg  3645  elabgf  3663  elabg  3665  reu6  3716  ru  3770  sbcbig  3822  unineq  4253  sbcnestgfw  4369  sbcnestgf  4374  preq12bg  4778  axrep1  5183  axrep4  5187  nalset  5209  opthg  5361  opelopabsb  5409  isso2i  5502  opeliunxp2  5703  resieq  5858  elimasng  5949  cbviotaw  6315  cbviota  6317  iota2df  6336  fnbrfvb  6712  fvelimab  6731  fvopab5  6793  fmptco  6884  fsng  6892  fressnfv  6915  fnpr2g  6965  isorel  7068  isocnv  7072  isocnv3  7074  isotr  7078  ovg  7302  caovcang  7338  caovordg  7344  caovord3d  7347  caovord  7348  orduninsuc  7546  opeliunxp2f  7867  brtpos  7892  dftpos4  7902  omopth  8275  ecopovsym  8389  xpf1o  8668  nneneq  8689  r1pwALT  9264  karden  9313  infxpenlem  9428  aceq0  9533  cflim2  9674  zfac  9871  ttukeylem1  9920  axextnd  10002  axrepndlem1  10003  axrepndlem2  10004  axrepnd  10005  axacndlem5  10022  zfcndrep  10025  zfcndac  10030  winalim  10106  gruina  10229  ltrnq  10390  ltsosr  10505  ltasr  10511  axpre-lttri  10576  axpre-ltadd  10578  nn0sub  11936  zextle  12044  zextlt  12045  xlesubadd  12646  sqeqor  13568  nn0opth2  13622  rexfiuz  14697  climshft  14923  rpnnen2lem10  15566  dvdsext  15661  ltoddhalfle  15700  halfleoddlt  15701  sumodd  15729  sadcadd  15797  dvdssq  15901  rpexp  16054  pcdvdsb  16195  imasleval  16804  isacs2  16914  acsfiel  16915  funcres2b  17157  pospropd  17734  isnsg  18247  nsgbi  18249  elnmz  18255  nmzbi  18256  oddvdsnn0  18603  odeq  18609  odmulg  18614  isslw  18664  slwispgp  18667  gsumval3lem2  18957  gsumcom2  19026  abveq0  19528  cnt0  21884  kqfvima  22268  kqt0lem  22274  isr0  22275  r0cld  22276  regr1lem2  22278  nrmr0reg  22287  isfildlem  22395  cnextfvval  22603  xmeteq0  22877  imasf1oxmet  22914  comet  23052  dscmet  23111  nrmmetd  23113  tngngp  23192  tngngp3  23194  mbfsup  24194  mbfinf  24195  degltlem1  24595  logltb  25110  cxple2  25207  rlimcnp  25471  rlimcnp2  25472  isppw2  25620  sqf11  25644  tgjustc1  26189  tgjustc2  26190  f1otrgitv  26584  nbuhgr2vtx1edgb  27062  dfconngr1  27895  eupth2lem3lem6  27940  nmlno0i  28499  nmlno0  28500  blocn  28512  ubth  28578  hvsubeq0  28773  hvaddcan  28775  hvsubadd  28782  normsub0  28841  hlim2  28897  pjoc1  29139  pjoc2  29144  chne0  29199  chsscon3  29205  chlejb1  29217  chnle  29219  h1de2ci  29261  elspansn  29271  elspansn2  29272  cmbr3  29313  cmcm  29319  cmcm3  29320  pjch1  29375  pjch  29399  pj11  29419  pjnel  29431  eigorth  29543  elnlfn  29633  nmlnop0  29703  lnopeq  29714  lnopcon  29740  lnfncon  29761  pjdifnormi  29872  chrelat2  30075  cvexch  30079  mdsym  30117  fmptcof2  30331  signswch  31731  cvmlift2lem12  32459  cvmlift2lem13  32460  satfv1lem  32507  satf0op  32522  fmlafvel  32530  abs2sqle  32821  abs2sqlt  32822  dfpo2  32889  eqfunresadj  32902  axextdist  32942  slerec  33175  brimageg  33286  brdomaing  33294  brrangeg  33295  elhf2  33534  nn0prpwlem  33568  nn0prpw  33569  onsuct0  33687  bj-sbceqgALT  34117  bj-ru0  34151  dfgcd3  34488  cbveud  34536  matunitlindf  34772  prdsbnd2  34956  isdrngo1  35117  eqrelf  35400  elsymrels5  35674  dfdisjs5  35827  eldisjs5  35841  lsatcmp  36021  llnexchb2  36887  lautset  37100  lautle  37102  zindbi  39423  wepwsolem  39522  aomclem8  39541  ntrneik13  40328  ntrneix13  40329  ntrneik4w  40330  2sbc6g  40627  2sbc5g  40628  wessf1ornlem  41325  fourierdlem31  42304  fourierdlem42  42315  fourierdlem54  42326  funressndmafv2rn  43303  dfatbrafv2b  43325  fnbrafv2b  43328  ichnfim  43471  sprsymrelf  43504  sprsymrelfo  43506  isomuspgrlem2b  43841  isomuspgrlem2d  43843  line2ylem  44636  line2xlem  44638
  Copyright terms: Public domain W3C validator