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  955  xorbi12d  1627  sb8eu  2641  cleqh  2862  vtoclb  3403  vtoclbg  3407  ceqsexg  3473  elabgf  3488  reu6  3536  ru  3575  sbcbig  3621  unineq  4020  sbcnestgf  4138  preq12bg  4530  prel12gOLD  4531  axrep1  4924  axrep4  4927  nalset  4947  opthg  5094  opelopabsb  5135  isso2i  5219  opeliunxp2  5416  resieq  5565  elimasng  5649  cbviota  6017  iota2df  6036  fnbrfvb  6398  fvelimab  6416  fvopab5  6473  fmptco  6560  fsng  6568  fsn2g  6569  fressnfv  6591  fnpr2g  6639  isorel  6740  isocnv  6744  isocnv3  6746  isotr  6750  ovg  6965  caovcang  7001  caovordg  7007  caovord3d  7010  caovord  7011  orduninsuc  7209  opeliunxp2f  7506  brtpos  7531  dftpos4  7541  omopth  7909  ecopovsym  8018  xpf1o  8289  nneneq  8310  r1pwALT  8884  karden  8933  infxpenlem  9046  aceq0  9151  cflim2  9297  zfac  9494  ttukeylem1  9543  axextnd  9625  axrepndlem1  9626  axrepndlem2  9627  axrepnd  9628  axacndlem5  9645  zfcndrep  9648  zfcndac  9653  winalim  9729  gruina  9852  ltrnq  10013  ltsosr  10127  ltasr  10133  axpre-lttri  10198  axpre-ltadd  10200  nn0sub  11555  zextle  11662  zextlt  11663  xlesubadd  12306  sqeqor  13192  nn0opth2  13273  rexfiuz  14306  climshft  14526  rpnnen2lem10  15171  dvdsext  15265  ltoddhalfle  15307  halfleoddlt  15308  sumodd  15333  sadcadd  15402  dvdssq  15502  rpexp  15654  pcdvdsb  15795  imasleval  16423  isacs2  16535  acsfiel  16536  funcres2b  16778  pospropd  17355  isnsg  17844  nsgbi  17846  elnmz  17854  nmzbi  17855  oddvdsnn0  18183  odeq  18189  odmulg  18193  isslw  18243  slwispgp  18246  gsumval3lem2  18527  gsumcom2  18594  abveq0  19048  cnt0  21372  kqfvima  21755  kqt0lem  21761  isr0  21762  r0cld  21763  regr1lem2  21765  nrmr0reg  21774  isfildlem  21882  cnextfvval  22090  xmeteq0  22364  imasf1oxmet  22401  comet  22539  dscmet  22598  nrmmetd  22600  tngngp  22679  tngngp3  22681  mbfsup  23650  mbfinf  23651  degltlem1  24051  logltb  24566  cxple2  24663  rlimcnp  24912  rlimcnp2  24913  isppw2  25061  sqf11  25085  f1otrgitv  25970  nbuhgr2vtx1edgb  26468  dfconngr1  27361  eupth2lem3lem6  27406  nmlno0i  27979  nmlno0  27980  blocn  27992  ubth  28059  hvsubeq0  28255  hvaddcan  28257  hvsubadd  28264  normsub0  28323  hlim2  28379  pjoc1  28623  pjoc2  28628  chne0  28683  chsscon3  28689  chlejb1  28701  chnle  28703  h1de2ci  28745  elspansn  28755  elspansn2  28756  cmbr3  28797  cmcm  28803  cmcm3  28804  pjch1  28859  pjch  28883  pj11  28903  pjnel  28915  eigorth  29027  elnlfn  29117  nmlnop0  29187  lnopeq  29198  lnopcon  29224  lnfncon  29245  pjdifnormi  29356  chrelat2  29559  cvexch  29563  mdsym  29601  fmptcof2  29787  signswch  30968  cvmlift2lem12  31624  cvmlift2lem13  31625  abs2sqle  31902  abs2sqlt  31903  dfpo2  31973  eqfunresadj  31987  br1steqgOLD  32000  br2ndeqgOLD  32001  axextdist  32031  slerec  32250  brimageg  32361  brdomaing  32369  brrangeg  32370  elhf2  32609  nn0prpwlem  32644  nn0prpw  32645  onsuct0  32767  bj-abbi  33103  bj-axrep1  33116  bj-axrep4  33119  bj-nalset  33122  bj-sbceqgALT  33219  bj-ru0  33257  dfgcd3  33499  matunitlindf  33738  prdsbnd2  33925  isdrngo1  34086  eqrelf  34362  elsymrels5  34643  lsatcmp  34811  llnexchb2  35676  lautset  35889  lautle  35891  zindbi  38031  wepwsolem  38132  aomclem8  38151  ntrneik13  38916  ntrneix13  38917  ntrneik4w  38918  2sbc6g  39136  2sbc5g  39137  wessf1ornlem  39888  fourierdlem31  40876  fourierdlem42  40887  fourierdlem54  40898  sprsymrelf  42273  sprsymrelfo  42275