Theorem bibi12d 334

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  bi2bian9  937  xorbi12d  1518  sb8eu  2532  cleqh  2753  vtoclb  3294  vtoclbg  3298  ceqsexg  3365  elabgf  3380  reu6  3428  ru  3467  sbcbig  3513  unineq  3910  sbcnestgf  4028  preq12bg  4417  prel12g  4418  axrep1  4805  axrep4  4808  nalset  4828  opthg  4975  opelopabsb  5014  isso2i  5096  opeliunxp2  5293  resieq  5442  elimasng  5526  cbviota  5894  iota2df  5913  fnbrfvb  6274  fvelimab  6292  fvopab5  6349  fmptco  6436  fsng  6444  fsn2g  6445  fressnfv  6467  fnpr2g  6515  isorel  6616  isocnv  6620  isocnv3  6622  isotr  6626  ovg  6841  caovcang  6877  caovordg  6883  caovord3d  6886  caovord  6887  orduninsuc  7085  opeliunxp2f  7381  brtpos  7406  dftpos4  7416  omopth  7783  ecopovsym  7892  xpf1o  8163  nneneq  8184  r1pwALT  8747  karden  8796  infxpenlem  8874  aceq0  8979  cflim2  9123  zfac  9320  ttukeylem1  9369  axextnd  9451  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axacndlem5  9471  zfcndrep  9474  zfcndac  9479  winalim  9555  gruina  9678  ltrnq  9839  ltsosr  9953  ltasr  9959  axpre-lttri  10024  axpre-ltadd  10026  nn0sub  11381  zextle  11488  zextlt  11489  xlesubadd  12131  sqeqor  13018  nn0opth2  13099  rexfiuz  14131  climshft  14351  rpnnen2lem10  14996  dvdsext  15090  ltoddhalfle  15132  halfleoddlt  15133  sumodd  15158  sadcadd  15227  dvdssq  15327  rpexp  15479  pcdvdsb  15620  imasleval  16248  isacs2  16361  acsfiel  16362  funcres2b  16604  pospropd  17181  isnsg  17670  nsgbi  17672  elnmz  17680  nmzbi  17681  oddvdsnn0  18009  odeq  18015  odmulg  18019  isslw  18069  slwispgp  18072  gsumval3lem2  18353  gsumcom2  18420  abveq0  18874  cnt0  21198  kqfvima  21581  kqt0lem  21587  isr0  21588  r0cld  21589  regr1lem2  21591  nrmr0reg  21600  isfildlem  21708  cnextfvval  21916  xmeteq0  22190  imasf1oxmet  22227  comet  22365  dscmet  22424  nrmmetd  22426  tngngp  22505  tngngp3  22507  mbfsup  23476  mbfinf  23477  degltlem1  23877  logltb  24391  cxple2  24488  rlimcnp  24737  rlimcnp2  24738  isppw2  24886  sqf11  24910  f1otrgitv  25795  nbuhgr2vtx1edgb  26293  dfconngr1  27166  eupth2lem3lem6  27211  nmlno0i  27777  nmlno0  27778  blocn  27790  ubth  27857  hvsubeq0  28053  hvaddcan  28055  hvsubadd  28062  normsub0  28121  hlim2  28177  pjoc1  28421  pjoc2  28426  chne0  28481  chsscon3  28487  chlejb1  28499  chnle  28501  h1de2ci  28543  elspansn  28553  elspansn2  28554  cmbr3  28595  cmcm  28601  cmcm3  28602  pjch1  28657  pjch  28681  pj11  28701  pjnel  28713  eigorth  28825  elnlfn  28915  nmlnop0  28985  lnopeq  28996  lnopcon  29022  lnfncon  29043  pjdifnormi  29154  chrelat2  29357  cvexch  29361  mdsym  29399  fmptcof2  29585  signswch  30766  cvmlift2lem12  31422  cvmlift2lem13  31423  abs2sqle  31700  abs2sqlt  31701  dfpo2  31771  eqfunresadj  31785  br1steqgOLD  31798  br2ndeqgOLD  31799  axextdist  31829  slerec  32048  brimageg  32159  brdomaing  32167  brrangeg  32168  elhf2  32407  nn0prpwlem  32442  nn0prpw  32443  onsuct0  32565  bj-abbi  32900  bj-axrep1  32913  bj-axrep4  32916  bj-nalset  32919  bj-sbceqgALT  33022  bj-ru0  33057  dfgcd3  33300  matunitlindf  33537  prdsbnd2  33724  isdrngo1  33885  eqrelf  34161  elsymrels5  34442  lsatcmp  34608  llnexchb2  35473  lautset  35686  lautle  35688  zindbi  37828  wepwsolem  37929  aomclem8  37948  ntrneik13  38713  ntrneix13  38714  ntrneik4w  38715  2sbc6g  38933  2sbc5g  38934  wessf1ornlem  39685  fourierdlem31  40673  fourierdlem42  40684  fourierdlem54  40695  sprsymrelf  42070  sprsymrelfo  42072