Theorem bibi12d 348

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

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bibi1d 346	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 345	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 281	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bi2bian9  639  xorbi12d  1514  norass  1529  sbbib  2376  sb8eulem  2680  abbi  2888  cleqh  2936  cleqf  3010  vtoclb  3565  vtoclbg  3569  ceqsexg  3646  elabgf  3664  elabg  3666  reu6  3717  ru  3771  sbcbig  3823  unineq  4254  sbcnestgfw  4370  sbcnestgf  4375  preq12bg  4778  axrep1  5184  axrep4  5188  nalset  5210  opthg  5362  opelopabsb  5410  isso2i  5503  opeliunxp2  5704  resieq  5859  elimasng  5950  cbviotaw  6316  cbviota  6318  iota2df  6337  fnbrfvb  6713  fvelimab  6732  fvopab5  6795  fmptco  6886  fsng  6894  fressnfv  6917  fnpr2g  6967  isorel  7073  isocnv  7077  isocnv3  7079  isotr  7083  ovg  7307  caovcang  7343  caovordg  7349  caovord3d  7352  caovord  7353  orduninsuc  7552  opeliunxp2f  7870  brtpos  7895  dftpos4  7905  omopth  8279  ecopovsym  8393  xpf1o  8673  nneneq  8694  r1pwALT  9269  karden  9318  infxpenlem  9433  aceq0  9538  cflim2  9679  zfac  9876  ttukeylem1  9925  axextnd  10007  axrepndlem1  10008  axrepndlem2  10009  axrepnd  10010  axacndlem5  10027  zfcndrep  10030  zfcndac  10035  winalim  10111  gruina  10234  ltrnq  10395  ltsosr  10510  ltasr  10516  axpre-lttri  10581  axpre-ltadd  10583  nn0sub  11941  zextle  12049  zextlt  12050  xlesubadd  12650  sqeqor  13572  nn0opth2  13626  rexfiuz  14701  climshft  14927  rpnnen2lem10  15570  dvdsext  15665  ltoddhalfle  15704  halfleoddlt  15705  sumodd  15733  sadcadd  15801  dvdssq  15905  rpexp  16058  pcdvdsb  16199  imasleval  16808  isacs2  16918  acsfiel  16919  funcres2b  17161  pospropd  17738  isnsg  18301  nsgbi  18303  elnmz  18309  nmzbi  18310  oddvdsnn0  18666  odeq  18672  odmulg  18677  isslw  18727  slwispgp  18730  gsumval3lem2  19020  gsumcom2  19089  abveq0  19591  cnt0  21948  kqfvima  22332  kqt0lem  22338  isr0  22339  r0cld  22340  regr1lem2  22342  nrmr0reg  22351  isfildlem  22459  cnextfvval  22667  xmeteq0  22942  imasf1oxmet  22979  comet  23117  dscmet  23176  nrmmetd  23178  tngngp  23257  tngngp3  23259  mbfsup  24259  mbfinf  24260  degltlem1  24660  logltb  25177  cxple2  25274  rlimcnp  25537  rlimcnp2  25538  isppw2  25686  sqf11  25710  tgjustc1  26255  tgjustc2  26256  f1otrgitv  26650  nbuhgr2vtx1edgb  27128  dfconngr1  27961  eupth2lem3lem6  28006  nmlno0i  28565  nmlno0  28566  blocn  28578  ubth  28644  hvsubeq0  28839  hvaddcan  28841  hvsubadd  28848  normsub0  28907  hlim2  28963  pjoc1  29205  pjoc2  29210  chne0  29265  chsscon3  29271  chlejb1  29283  chnle  29285  h1de2ci  29327  elspansn  29337  elspansn2  29338  cmbr3  29379  cmcm  29385  cmcm3  29386  pjch1  29441  pjch  29465  pj11  29485  pjnel  29497  eigorth  29609  elnlfn  29699  nmlnop0  29769  lnopeq  29780  lnopcon  29806  lnfncon  29827  pjdifnormi  29938  chrelat2  30141  cvexch  30145  mdsym  30183  fmptcof2  30396  signswch  31826  cvmlift2lem12  32556  cvmlift2lem13  32557  satfv1lem  32604  satf0op  32619  fmlafvel  32627  abs2sqle  32918  abs2sqlt  32919  dfpo2  32986  eqfunresadj  32999  axextdist  33039  slerec  33272  brimageg  33383  brdomaing  33391  brrangeg  33392  elhf2  33631  nn0prpwlem  33665  nn0prpw  33666  onsuct0  33784  bj-sbceqgALT  34214  bj-ru0  34248  dfgcd3  34599  cbveud  34647  matunitlindf  34884  prdsbnd2  35067  isdrngo1  35228  eqrelf  35511  elsymrels5  35786  dfdisjs5  35939  eldisjs5  35953  lsatcmp  36133  llnexchb2  36999  lautset  37212  lautle  37214  zindbi  39536  wepwsolem  39635  aomclem8  39654  ntrneik13  40441  ntrneix13  40442  ntrneik4w  40443  2sbc6g  40740  2sbc5g  40741  wessf1ornlem  41437  fourierdlem31  42416  fourierdlem42  42427  fourierdlem54  42438  funressndmafv2rn  43415  dfatbrafv2b  43437  fnbrafv2b  43440  ichnfim  43617  sprsymrelf  43650  sprsymrelfo  43652  isomuspgrlem2b  43987  isomuspgrlem2d  43989  line2ylem  44731  line2xlem  44733