Theorem bibi12d 338

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bi2bian9  628  xorbi12d  1502  sbbib  2294  sb8eulem  2632  cleqh  2890  cleqf  2962  vtoclb  3484  vtoclbg  3488  ceqsexg  3562  elabgf  3579  elabg  3581  reu6  3630  ru  3681  sbcbig  3728  unineq  4142  sbcnestgf  4259  preq12bg  4658  axrep1  5050  axrep4  5054  nalset  5074  opthg  5226  opelopabsb  5271  isso2i  5360  opeliunxp2  5559  resieq  5709  elimasng  5795  cbviota  6157  iota2df  6176  fnbrfvb  6548  fvelimab  6566  fvopab5  6625  fmptco  6714  fsng  6722  fressnfv  6745  fnpr2g  6799  isorel  6902  isocnv  6906  isocnv3  6908  isotr  6912  ovg  7129  caovcang  7165  caovordg  7171  caovord3d  7174  caovord  7175  orduninsuc  7374  opeliunxp2f  7679  brtpos  7704  dftpos4  7714  omopth  8085  ecopovsym  8199  xpf1o  8475  nneneq  8496  r1pwALT  9069  karden  9118  infxpenlem  9233  aceq0  9338  cflim2  9483  zfac  9680  ttukeylem1  9729  axextnd  9811  axrepndlem1  9812  axrepndlem2  9813  axrepnd  9814  axacndlem5  9831  zfcndrep  9834  zfcndac  9839  winalim  9915  gruina  10038  ltrnq  10199  ltsosr  10314  ltasr  10320  axpre-lttri  10385  axpre-ltadd  10387  nn0sub  11759  zextle  11868  zextlt  11869  xlesubadd  12472  sqeqor  13393  nn0opth2  13447  rexfiuz  14568  climshft  14794  rpnnen2lem10  15436  dvdsext  15531  ltoddhalfle  15570  halfleoddlt  15571  sumodd  15599  sadcadd  15667  dvdssq  15767  rpexp  15920  pcdvdsb  16061  imasleval  16670  isacs2  16782  acsfiel  16783  funcres2b  17025  pospropd  17602  isnsg  18092  nsgbi  18094  elnmz  18102  nmzbi  18103  oddvdsnn0  18434  odeq  18440  odmulg  18444  isslw  18494  slwispgp  18497  gsumval3lem2  18780  gsumcom2  18848  abveq0  19319  cnt0  21658  kqfvima  22042  kqt0lem  22048  isr0  22049  r0cld  22050  regr1lem2  22052  nrmr0reg  22061  isfildlem  22169  cnextfvval  22377  xmeteq0  22651  imasf1oxmet  22688  comet  22826  dscmet  22885  nrmmetd  22887  tngngp  22966  tngngp3  22968  mbfsup  23968  mbfinf  23969  degltlem1  24369  logltb  24884  cxple2  24981  rlimcnp  25245  rlimcnp2  25246  isppw2  25394  sqf11  25418  tgjustc1  25963  tgjustc2  25964  f1otrgitv  26359  nbuhgr2vtx1edgb  26837  dfconngr1  27717  eupth2lem3lem6  27763  nmlno0i  28348  nmlno0  28349  blocn  28361  ubth  28428  hvsubeq0  28624  hvaddcan  28626  hvsubadd  28633  normsub0  28692  hlim2  28748  pjoc1  28992  pjoc2  28997  chne0  29052  chsscon3  29058  chlejb1  29070  chnle  29072  h1de2ci  29114  elspansn  29124  elspansn2  29125  cmbr3  29166  cmcm  29172  cmcm3  29173  pjch1  29228  pjch  29252  pj11  29272  pjnel  29284  eigorth  29396  elnlfn  29486  nmlnop0  29556  lnopeq  29567  lnopcon  29593  lnfncon  29614  pjdifnormi  29725  chrelat2  29928  cvexch  29932  mdsym  29970  fmptcof2  30164  signswch  31474  cvmlift2lem12  32143  cvmlift2lem13  32144  satf0op  32184  fmlafvel  32192  abs2sqle  32440  abs2sqlt  32441  dfpo2  32508  eqfunresadj  32521  axextdist  32562  slerec  32795  brimageg  32906  brdomaing  32914  brrangeg  32915  elhf2  33154  nn0prpwlem  33188  nn0prpw  33189  onsuct0  33306  bj-abbi  33604  bj-axrep1  33615  bj-axrep4  33618  bj-sbceqgALT  33708  bj-ru0  33745  dfgcd3  34044  cbveud  34092  matunitlindf  34328  prdsbnd2  34512  isdrngo1  34673  eqrelf  34958  elsymrels5  35234  dfdisjs5  35387  eldisjs5  35401  lsatcmp  35581  llnexchb2  36447  lautset  36660  lautle  36662  zindbi  38936  wepwsolem  39035  aomclem8  39054  ntrneik13  39808  ntrneix13  39809  ntrneik4w  39810  2sbc6g  40161  2sbc5g  40162  wessf1ornlem  40867  fourierdlem31  41852  fourierdlem42  41863  fourierdlem54  41874  funressndmafv2rn  42826  dfatbrafv2b  42848  fnbrafv2b  42851  ichnfim  42992  sprsymrelf  43023  sprsymrelfo  43025  isomuspgrlem2b  43360  isomuspgrlem2d  43362  line2ylem  44104  line2xlem  44106