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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  bi2bian9  915  xorbi12d  1470  sb8eu  2491  cleqh  2711  vtoclb  3236  vtoclbg  3240  ceqsexg  3304  elabgf  3317  reu6  3362  ru  3401  sbcbig  3447  unineq  3836  sbcnestgf  3947  preq12bg  4326  prel12g  4327  axrep1  4700  axrep4  4703  nalset  4723  opthg  4872  opelopabsb  4910  isso2i  4991  opeliunxp2  5182  resieq  5327  elimasng  5410  cbviota  5773  iota2df  5792  fnbrfvb  6146  fvelimab  6163  fvopab5  6217  fmptco  6303  fsng  6310  fsn2g  6311  fressnfv  6332  fnpr2g  6379  isorel  6476  isocnv  6480  isocnv3  6482  isotr  6486  ovg  6697  caovcang  6733  caovordg  6739  caovord3d  6742  caovord  6743  orduninsuc  6935  opeliunxp2f  7223  brtpos  7248  dftpos4  7258  omopth  7625  ecopovsym  7736  xpf1o  8007  nneneq  8028  r1pwALT  8592  karden  8641  infxpenlem  8719  aceq0  8824  cflim2  8968  zfac  9165  ttukeylem1  9214  axextnd  9292  axrepndlem1  9293  axrepndlem2  9294  axrepnd  9295  axacndlem5  9312  zfcndrep  9315  zfcndac  9320  winalim  9396  gruina  9519  ltrnq  9680  ltsosr  9794  ltasr  9800  axpre-lttri  9865  axpre-ltadd  9867  nn0sub  11220  zextle  11326  zextlt  11327  xlesubadd  11965  sqeqor  12840  nn0opth2  12921  rexfiuz  13935  climshft  14155  rpnnen2lem10  14791  dvdsext  14881  ltoddhalfle  14923  halfleoddlt  14924  sumodd  14949  sadcadd  15018  dvdssq  15118  isprm2lem  15232  rpexp  15270  pcdvdsb  15411  imasleval  16024  isacs2  16137  acsfiel  16138  funcres2b  16380  pospropd  16957  isnsg  17446  nsgbi  17448  elnmz  17456  nmzbi  17457  oddvdsnn0  17786  odeq  17792  odmulg  17796  isslw  17846  slwispgp  17849  gsumval3lem2  18130  gsumcom2  18197  abveq0  18649  cnt0  20960  kqfvima  21343  kqt0lem  21349  isr0  21350  r0cld  21351  regr1lem2  21353  nrmr0reg  21362  isfildlem  21471  cnextfvval  21679  xmeteq0  21953  imasf1oxmet  21990  comet  22128  dscmet  22187  nrmmetd  22189  tngngp  22268  tngngp3  22270  mbfsup  23237  mbfinf  23238  degltlem1  23636  logltb  24150  cxple2  24243  rlimcnp  24492  rlimcnp2  24493  isppw2  24641  sqf11  24665  f1otrgitv  25550  isrgrac  26461  eupath2lem3  26506  nmlno0i  27033  nmlno0  27034  blocn  27046  ubth  27113  hvsubeq0  27309  hvaddcan  27311  hvsubadd  27318  normsub0  27377  hlim2  27433  pjoc1  27677  pjoc2  27682  chne0  27737  chsscon3  27743  chlejb1  27755  chnle  27757  h1de2ci  27799  elspansn  27809  elspansn2  27810  cmbr3  27851  cmcm  27857  cmcm3  27858  pjch1  27913  pjch  27937  pj11  27957  pjnel  27969  eigorth  28081  elnlfn  28171  nmlnop0  28241  lnopeq  28252  lnopcon  28278  lnfncon  28299  pjdifnormi  28410  chrelat2  28613  cvexch  28617  mdsym  28655  fmptcof2  28839  signswch  29964  cvmlift2lem12  30550  cvmlift2lem13  30551  abs2sqle  30828  abs2sqlt  30829  dfpo2  30898  br1steqg  30919  br2ndeqg  30920  axextdist  30949  brimageg  31204  brdomaing  31212  brrangeg  31213  elhf2  31452  nn0prpwlem  31487  nn0prpw  31488  onsuct0  31610  bj-abbi  31963  bj-axrep1  31976  bj-axrep4  31979  bj-nalset  31982  bj-sbceqgALT  32089  bj-ru0  32124  matunitlindf  32577  prdsbnd2  32764  isdrngo1  32925  lsatcmp  33308  llnexchb2  34173  lautset  34386  lautle  34388  zindbi  36529  wepwsolem  36630  aomclem8  36649  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  2sbc6g  37638  2sbc5g  37639  dfcleqf  38281  wessf1ornlem  38366  fourierdlem31  39031  fourierdlem42  39042  fourierdlem54  39053  nbuhgr2vtx1edgb  40574  dfconngr1  41355  eupth2lem3lem6  41401