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 279	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bi2bian9  640  xorbi12d  1525  norass  1537  ru0  2128  sbbib  2359  sb8eulem  2591  abbib  2798  cleqh  2857  cleqf  2920  vtoclbg  3523  vtoclb  3534  ceqsexg  3619  elabgf  3641  reu6  3697  ruOLD  3752  sbcbig  3805  unineq  4251  sbcnestgfw  4384  sbcnestgf  4389  preq12bg  4817  axrep1  5235  axrep4OLD  5241  nalset  5268  opthg  5437  opelopabsb  5490  isso2i  5583  opeliunxp2  5802  resieq  5961  dfpo2  6269  cbviotaw  6471  cbviota  6473  iota2df  6498  fnbrfvb  6911  fvelimab  6933  fvopab5  7001  fmptco  7101  fsng  7109  fressnfv  7132  fnpr2g  7184  isorel  7301  isocnv  7305  isocnv3  7307  isotr  7311  eqfunresadj  7335  ovg  7554  caovcang  7590  caovordg  7596  caovord3d  7599  caovord  7600  caofidlcan  7691  orduninsuc  7819  xpord2pred  8124  xpord3pred  8131  opeliunxp2f  8189  brtpos  8214  dftpos4  8224  omopth  8626  ecopovsym  8792  xpf1o  9103  nneneq  9170  ttrclselem2  9679  r1pwALT  9799  karden  9848  infxpenlem  9966  aceq0  10071  cflim2  10216  zfac  10413  ttukeylem1  10462  axextnd  10544  axrepndlem1  10545  axrepndlem2  10546  axrepnd  10547  axacndlem5  10564  zfcndrep  10567  zfcndac  10572  winalim  10648  gruina  10771  ltrnq  10932  ltsosr  11047  ltasr  11053  axpre-lttri  11118  axpre-ltadd  11120  nn0sub  12492  zextle  12607  zextlt  12608  xlesubadd  13223  sqeqor  14181  nn0opth2  14237  rexfiuz  15314  climshft  15542  rpnnen2lem10  16191  dvdsext  16291  ltoddhalfle  16331  halfleoddlt  16332  sumodd  16358  sadcadd  16428  dvdssq  16537  rpexp  16692  pcdvdsb  16840  imasleval  17504  isacs2  17614  acsfiel  17615  funcres2b  17859  pospropd  18286  isnsg  19087  nsgbi  19089  elnmz  19095  nmzbi  19096  oddvdsnn0  19474  odeq  19480  odmulg  19486  isslw  19538  slwispgp  19541  gsumval3lem2  19836  gsumcom2  19905  abveq0  20727  cnt0  23233  kqfvima  23617  kqt0lem  23623  isr0  23624  r0cld  23625  regr1lem2  23627  nrmr0reg  23636  isfildlem  23744  cnextfvval  23952  xmeteq0  24226  imasf1oxmet  24263  comet  24401  dscmet  24460  nrmmetd  24462  tngngp  24542  tngngp3  24544  mbfsup  25565  mbfinf  25566  degltlem1  25977  logltb  26509  cxple2  26606  rlimcnp  26875  rlimcnp2  26876  isppw2  27025  sqf11  27049  slerec  27731  tgjustc1  28402  tgjustc2  28403  f1otrgitv  28797  nbuhgr2vtx1edgb  29279  dfconngr1  30117  eupth2lem3lem6  30162  nmlno0i  30723  nmlno0  30724  blocn  30736  ubth  30802  hvsubeq0  30997  hvaddcan  30999  hvsubadd  31006  normsub0  31065  hlim2  31121  pjoc1  31363  pjoc2  31368  chne0  31423  chsscon3  31429  chlejb1  31441  chnle  31443  h1de2ci  31485  elspansn  31495  elspansn2  31496  cmbr3  31537  cmcm  31543  cmcm3  31544  pjch1  31599  pjch  31623  pj11  31643  pjnel  31655  eigorth  31767  elnlfn  31857  nmlnop0  31927  lnopeq  31938  lnopcon  31964  lnfncon  31985  pjdifnormi  32096  chrelat2  32299  cvexch  32303  mdsym  32341  eqelbid  32404  fmptcof2  32581  mgcoval  32912  mgcval  32913  mgccole1  32916  mgccole2  32917  mgcmnt1  32918  mgcmnt2  32919  mgccnv  32925  unitprodclb  33360  ist0cld  33823  zarclssn  33863  zart0  33869  signswch  34552  fnrelpredd  35079  cvmlift2lem12  35301  cvmlift2lem13  35302  satfv1lem  35349  satf0op  35364  fmlafvel  35372  abs2sqle  35667  abs2sqlt  35668  axextdist  35787  brimageg  35915  brdomaing  35923  brrangeg  35924  elhf2  36163  nn0prpwlem  36310  nn0prpw  36311  onsuct0  36429  bj-sbceqgALT  36890  bj-elabd2ALT  36913  eleq2w2ALT  37035  dfgcd3  37312  cbveud  37360  wl-3xorbi123d  37463  matunitlindf  37612  prdsbnd2  37789  isdrngo1  37950  eqrelf  38244  elsymrels5  38547  dfdisjs5  38704  eldisjs5  38718  mpets2  38833  pets  38844  lsatcmp  38996  llnexchb2  39863  lautset  40076  lautle  40078  sticksstones2  42135  aks6d1c7  42172  dvdsexpnn0  42322  eu6w  42664  abbibw  42665  zindbi  42935  wepwsolem  43031  aomclem8  43050  onsupmaxb  43228  oaordnr  43285  omnord1  43294  oenord1  43305  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  2sbc6g  44404  2sbc5g  44405  modelaxreplem3  44970  wessf1ornlem  45179  fourierdlem31  46136  fourierdlem42  46147  fourierdlem54  46158  funressndmafv2rn  47224  dfatbrafv2b  47246  fnbrafv2b  47249  ichbidv  47454  ichnfim  47465  sprsymrelf  47496  sprsymrelfo  47498  isuspgrimlem  47895  line2ylem  48740  line2xlem  48742  mofeu  48836  tposres0  48865  catprslem  48999