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 278	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  639  xorbi12d  1525  norass  1538  sbbib  2357  sb8eulem  2592  abbib  2804  cleqh  2863  cleqf  2934  vtoclb  3553  vtoclbg  3559  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  7325  isocnv  7329  isocnv3  7331  isotr  7335  eqfunresadj  7359  ovg  7574  caovcang  7610  caovordg  7616  caovord3d  7619  caovord  7620  orduninsuc  7834  xpord2pred  8133  xpord3pred  8140  opeliunxp2f  8197  brtpos  8222  dftpos4  8232  omopth  8663  ecopovsym  8815  xpf1o  9141  nneneq  9211  nneneqOLD  9223  ttrclselem2  9723  r1pwALT  9843  karden  9892  infxpenlem  10010  aceq0  10115  cflim2  10260  zfac  10457  ttukeylem1  10506  axextnd  10588  axrepndlem1  10589  axrepndlem2  10590  axrepnd  10591  axacndlem5  10608  zfcndrep  10611  zfcndac  10616  winalim  10692  gruina  10815  ltrnq  10976  ltsosr  11091  ltasr  11097  axpre-lttri  11162  axpre-ltadd  11164  nn0sub  12526  zextle  12639  zextlt  12640  xlesubadd  13246  sqeqor  14184  nn0opth2  14236  rexfiuz  15298  climshft  15524  rpnnen2lem10  16170  dvdsext  16268  ltoddhalfle  16308  halfleoddlt  16309  sumodd  16335  sadcadd  16403  dvdssq  16508  rpexp  16663  pcdvdsb  16806  imasleval  17491  isacs2  17601  acsfiel  17602  funcres2b  17851  pospropd  18284  isnsg  19071  nsgbi  19073  elnmz  19079  nmzbi  19080  oddvdsnn0  19453  odeq  19459  odmulg  19465  isslw  19517  slwispgp  19520  gsumval3lem2  19815  gsumcom2  19884  abveq0  20577  cnt0  23070  kqfvima  23454  kqt0lem  23460  isr0  23461  r0cld  23462  regr1lem2  23464  nrmr0reg  23473  isfildlem  23581  cnextfvval  23789  xmeteq0  24064  imasf1oxmet  24101  comet  24242  dscmet  24301  nrmmetd  24303  tngngp  24391  tngngp3  24393  mbfsup  25405  mbfinf  25406  degltlem1  25814  logltb  26332  cxple2  26429  rlimcnp  26694  rlimcnp2  26695  isppw2  26843  sqf11  26867  slerec  27545  tgjustc1  27981  tgjustc2  27982  f1otrgitv  28376  nbuhgr2vtx1edgb  28864  dfconngr1  29696  eupth2lem3lem6  29741  nmlno0i  30302  nmlno0  30303  blocn  30315  ubth  30381  hvsubeq0  30576  hvaddcan  30578  hvsubadd  30585  normsub0  30644  hlim2  30700  pjoc1  30942  pjoc2  30947  chne0  31002  chsscon3  31008  chlejb1  31020  chnle  31022  h1de2ci  31064  elspansn  31074  elspansn2  31075  cmbr3  31116  cmcm  31122  cmcm3  31123  pjch1  31178  pjch  31202  pj11  31222  pjnel  31234  eigorth  31346  elnlfn  31436  nmlnop0  31506  lnopeq  31517  lnopcon  31543  lnfncon  31564  pjdifnormi  31675  chrelat2  31878  cvexch  31882  mdsym  31920  eqelbid  31970  fmptcof2  32137  mgcoval  32411  mgcval  32412  mgccole1  32415  mgccole2  32416  mgcmnt1  32417  mgcmnt2  32418  mgccnv  32424  ist0cld  33099  zarclssn  33139  zart0  33145  signswch  33858  fnrelpredd  34378  cvmlift2lem12  34591  cvmlift2lem13  34592  satfv1lem  34639  satf0op  34654  fmlafvel  34662  abs2sqle  34951  abs2sqlt  34952  axextdist  35063  brimageg  35191  brdomaing  35199  brrangeg  35200  elhf2  35439  nn0prpwlem  35510  nn0prpw  35511  onsuct0  35629  bj-sbceqgALT  36085  bj-elabd2ALT  36108  bj-ru0  36126  eleq2w2ALT  36231  dfgcd3  36508  cbveud  36556  wl-3xorbi123d  36659  matunitlindf  36789  prdsbnd2  36966  isdrngo1  37127  eqrelf  37426  elsymrels5  37729  dfdisjs5  37885  eldisjs5  37899  mpets2  38014  pets  38025  lsatcmp  38176  llnexchb2  39043  lautset  39256  lautle  39258  sticksstones2  41269  dvdsexpnn0  41534  zindbi  41987  wepwsolem  42086  aomclem8  42105  onsupmaxb  42290  oaordnr  42348  omnord1  42357  oenord1  42368  ntrneik13  43151  ntrneix13  43152  ntrneik4w  43153  2sbc6g  43476  2sbc5g  43477  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