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 205

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 206

This theorem is referenced by:  bi2bian9  638  xorbi12d  1524  norass  1537  sbbib  2356  sb8eulem  2591  abbib  2803  cleqh  2862  cleqf  2933  vtoclbg  3544  vtoclb  3556  ceqsexg  3641  elabgf  3664  elabgOLD  3667  reu6  3722  ru  3776  sbcbig  3831  unineq  4277  sbcnestgfw  4418  sbcnestgf  4423  preq12bg  4854  axrep1  5286  axrep4  5290  nalset  5313  opthg  5477  opelopabsb  5530  isso2i  5623  opeliunxp2  5838  resieq  5992  elimasngOLD  6089  dfpo2  6295  cbviotaw  6502  cbviota  6505  iota2df  6530  fnbrfvb  6944  fvelimab  6964  fvopab5  7030  fmptco  7129  fsng  7137  fressnfv  7160  fnpr2g  7214  isorel  7326  isocnv  7330  isocnv3  7332  isotr  7336  eqfunresadj  7360  ovg  7575  caovcang  7611  caovordg  7617  caovord3d  7620  caovord  7621  orduninsuc  7835  xpord2pred  8134  xpord3pred  8141  opeliunxp2f  8198  brtpos  8223  dftpos4  8233  omopth  8664  ecopovsym  8816  xpf1o  9142  nneneq  9212  nneneqOLD  9224  ttrclselem2  9724  r1pwALT  9844  karden  9893  infxpenlem  10011  aceq0  10116  cflim2  10261  zfac  10458  ttukeylem1  10507  axextnd  10589  axrepndlem1  10590  axrepndlem2  10591  axrepnd  10592  axacndlem5  10609  zfcndrep  10612  zfcndac  10617  winalim  10693  gruina  10816  ltrnq  10977  ltsosr  11092  ltasr  11098  axpre-lttri  11163  axpre-ltadd  11165  nn0sub  12527  zextle  12640  zextlt  12641  xlesubadd  13247  sqeqor  14185  nn0opth2  14237  rexfiuz  15299  climshft  15525  rpnnen2lem10  16171  dvdsext  16269  ltoddhalfle  16309  halfleoddlt  16310  sumodd  16336  sadcadd  16404  dvdssq  16509  rpexp  16664  pcdvdsb  16807  imasleval  17492  isacs2  17602  acsfiel  17603  funcres2b  17852  pospropd  18285  isnsg  19072  nsgbi  19074  elnmz  19080  nmzbi  19081  oddvdsnn0  19454  odeq  19460  odmulg  19466  isslw  19518  slwispgp  19521  gsumval3lem2  19816  gsumcom2  19885  abveq0  20578  cnt0  23071  kqfvima  23455  kqt0lem  23461  isr0  23462  r0cld  23463  regr1lem2  23465  nrmr0reg  23474  isfildlem  23582  cnextfvval  23790  xmeteq0  24065  imasf1oxmet  24102  comet  24243  dscmet  24302  nrmmetd  24304  tngngp  24392  tngngp3  24394  mbfsup  25414  mbfinf  25415  degltlem1  25826  logltb  26345  cxple2  26442  rlimcnp  26707  rlimcnp2  26708  isppw2  26856  sqf11  26880  slerec  27558  tgjustc1  27994  tgjustc2  27995  f1otrgitv  28389  nbuhgr2vtx1edgb  28877  dfconngr1  29709  eupth2lem3lem6  29754  nmlno0i  30315  nmlno0  30316  blocn  30328  ubth  30394  hvsubeq0  30589  hvaddcan  30591  hvsubadd  30598  normsub0  30657  hlim2  30713  pjoc1  30955  pjoc2  30960  chne0  31015  chsscon3  31021  chlejb1  31033  chnle  31035  h1de2ci  31077  elspansn  31087  elspansn2  31088  cmbr3  31129  cmcm  31135  cmcm3  31136  pjch1  31191  pjch  31215  pj11  31235  pjnel  31247  eigorth  31359  elnlfn  31449  nmlnop0  31519  lnopeq  31530  lnopcon  31556  lnfncon  31577  pjdifnormi  31688  chrelat2  31891  cvexch  31895  mdsym  31933  eqelbid  31983  fmptcof2  32150  mgcoval  32424  mgcval  32425  mgccole1  32428  mgccole2  32429  mgcmnt1  32430  mgcmnt2  32431  mgccnv  32437  ist0cld  33112  zarclssn  33152  zart0  33158  signswch  33871  fnrelpredd  34391  cvmlift2lem12  34604  cvmlift2lem13  34605  satfv1lem  34652  satf0op  34667  fmlafvel  34675  abs2sqle  34964  abs2sqlt  34965  axextdist  35076  brimageg  35204  brdomaing  35212  brrangeg  35213  elhf2  35452  nn0prpwlem  35511  nn0prpw  35512  onsuct0  35630  bj-sbceqgALT  36086  bj-elabd2ALT  36109  bj-ru0  36127  eleq2w2ALT  36232  dfgcd3  36509  cbveud  36557  wl-3xorbi123d  36660  matunitlindf  36790  prdsbnd2  36967  isdrngo1  37128  eqrelf  37427  elsymrels5  37730  dfdisjs5  37886  eldisjs5  37900  mpets2  38015  pets  38026  lsatcmp  38177  llnexchb2  39044  lautset  39257  lautle  39259  sticksstones2  41270  dvdsexpnn0  41535  zindbi  41988  wepwsolem  42087  aomclem8  42106  onsupmaxb  42291  oaordnr  42349  omnord1  42358  oenord1  42369  ntrneik13  43152  ntrneix13  43153  ntrneik4w  43154  2sbc6g  43477  2sbc5g  43478  wessf1ornlem  44183  fourierdlem31  45153  fourierdlem42  45164  fourierdlem54  45175  funressndmafv2rn  46230  dfatbrafv2b  46252  fnbrafv2b  46255  ichbidv  46420  ichnfim  46431  sprsymrelf  46462  sprsymrelfo  46464  isomuspgrlem2b  46796  isomuspgrlem2d  46798  line2ylem  47525  line2xlem  47527  mofeu  47602  catprslem  47718