Theorem bibi12d 345

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 343	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 342	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 278	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bi2bian9  637  xorbi12d  1521  norass  1537  sbbib  2360  sb8eulem  2599  abbi  2811  cleqh  2863  clelab  2884  cleqf  2939  vtoclb  3500  vtoclbg  3505  ceqsexg  3583  elabgf  3606  elabgOLD  3609  reu6  3664  ru  3718  sbcbig  3773  unineq  4216  sbcnestgfw  4357  sbcnestgf  4362  preq12bg  4789  axrep1  5214  axrep4  5218  nalset  5240  opthg  5394  opelopabsb  5444  isso2i  5537  opeliunxp2  5744  resieq  5899  elimasngOLD  5995  dfpo2  6196  cbviotaw  6395  cbviota  6398  iota2df  6417  fnbrfvb  6816  fvelimab  6835  fvopab5  6901  fmptco  6995  fsng  7003  fressnfv  7026  fnpr2g  7080  isorel  7190  isocnv  7194  isocnv3  7196  isotr  7200  ovg  7428  caovcang  7464  caovordg  7470  caovord3d  7473  caovord  7474  orduninsuc  7678  opeliunxp2f  8010  brtpos  8035  dftpos4  8045  omopth  8466  ecopovsym  8582  xpf1o  8891  nneneq  8956  nneneqOLD  8969  ttrclselem2  9445  r1pwALT  9588  karden  9637  infxpenlem  9753  aceq0  9858  cflim2  10003  zfac  10200  ttukeylem1  10249  axextnd  10331  axrepndlem1  10332  axrepndlem2  10333  axrepnd  10334  axacndlem5  10351  zfcndrep  10354  zfcndac  10359  winalim  10435  gruina  10558  ltrnq  10719  ltsosr  10834  ltasr  10840  axpre-lttri  10905  axpre-ltadd  10907  nn0sub  12266  zextle  12376  zextlt  12377  xlesubadd  12979  sqeqor  13913  nn0opth2  13967  rexfiuz  15040  climshft  15266  rpnnen2lem10  15913  dvdsext  16011  ltoddhalfle  16051  halfleoddlt  16052  sumodd  16078  sadcadd  16146  dvdssq  16253  rpexp  16408  pcdvdsb  16551  imasleval  17233  isacs2  17343  acsfiel  17344  funcres2b  17593  pospropd  18026  isnsg  18764  nsgbi  18766  elnmz  18772  nmzbi  18773  oddvdsnn0  19133  odeq  19139  odmulg  19144  isslw  19194  slwispgp  19197  gsumval3lem2  19488  gsumcom2  19557  abveq0  20067  cnt0  22478  kqfvima  22862  kqt0lem  22868  isr0  22869  r0cld  22870  regr1lem2  22872  nrmr0reg  22881  isfildlem  22989  cnextfvval  23197  xmeteq0  23472  imasf1oxmet  23509  comet  23650  dscmet  23709  nrmmetd  23711  tngngp  23799  tngngp3  23801  mbfsup  24809  mbfinf  24810  degltlem1  25218  logltb  25736  cxple2  25833  rlimcnp  26096  rlimcnp2  26097  isppw2  26245  sqf11  26269  tgjustc1  26817  tgjustc2  26818  f1otrgitv  27212  nbuhgr2vtx1edgb  27700  dfconngr1  28531  eupth2lem3lem6  28576  nmlno0i  29135  nmlno0  29136  blocn  29148  ubth  29214  hvsubeq0  29409  hvaddcan  29411  hvsubadd  29418  normsub0  29477  hlim2  29533  pjoc1  29775  pjoc2  29780  chne0  29835  chsscon3  29841  chlejb1  29853  chnle  29855  h1de2ci  29897  elspansn  29907  elspansn2  29908  cmbr3  29949  cmcm  29955  cmcm3  29956  pjch1  30011  pjch  30035  pj11  30055  pjnel  30067  eigorth  30179  elnlfn  30269  nmlnop0  30339  lnopeq  30350  lnopcon  30376  lnfncon  30397  pjdifnormi  30508  chrelat2  30711  cvexch  30715  mdsym  30753  fmptcof2  30973  mgcoval  31243  mgcval  31244  mgccole1  31247  mgccole2  31248  mgcmnt1  31249  mgcmnt2  31250  mgccnv  31256  ist0cld  31762  zarclssn  31802  zart0  31808  signswch  32519  fnrelpredd  33040  cvmlift2lem12  33255  cvmlift2lem13  33256  satfv1lem  33303  satf0op  33318  fmlafvel  33326  abs2sqle  33617  abs2sqlt  33618  eqfunresadj  33714  axextdist  33754  xpord2pred  33771  xpord3pred  33777  slerec  33992  brimageg  34208  brdomaing  34216  brrangeg  34217  elhf2  34456  nn0prpwlem  34490  nn0prpw  34491  onsuct0  34609  bj-sbceqgALT  35066  bj-elabd2ALT  35092  bj-ru0  35110  eleq2w2ALT  35199  dfgcd3  35474  cbveud  35522  wl-3xorbi123d  35625  matunitlindf  35754  prdsbnd2  35932  isdrngo1  36093  eqrelf  36374  elsymrels5  36649  dfdisjs5  36802  eldisjs5  36816  lsatcmp  36996  llnexchb2  37862  lautset  38075  lautle  38077  sticksstones2  40083  dvdsexpnn0  40321  zindbi  40748  wepwsolem  40847  aomclem8  40866  ntrneik13  41661  ntrneix13  41662  ntrneik4w  41663  2sbc6g  41986  2sbc5g  41987  wessf1ornlem  42675  fourierdlem31  43633  fourierdlem42  43644  fourierdlem54  43655  funressndmafv2rn  44666  dfatbrafv2b  44688  fnbrafv2b  44691  ichbidv  44857  ichnfim  44868  sprsymrelf  44899  sprsymrelfo  44901  isomuspgrlem2b  45233  isomuspgrlem2d  45235  line2ylem  46049  line2xlem  46051  mofeu  46127  catprslem  46243