Theorem bibi12d 344

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 342	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 341	. 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  637  xorbi12d  1523  norass  1536  sbbib  2355  sb8eulem  2590  abbib  2802  cleqh  2861  cleqf  2932  vtoclbg  3543  vtoclb  3555  ceqsexg  3640  elabgf  3663  elabgOLD  3666  reu6  3721  ru  3775  sbcbig  3830  unineq  4276  sbcnestgfw  4417  sbcnestgf  4422  preq12bg  4853  axrep1  5285  axrep4  5289  nalset  5312  opthg  5476  opelopabsb  5529  isso2i  5622  opeliunxp2  5837  resieq  5991  elimasngOLD  6088  dfpo2  6294  cbviotaw  6501  cbviota  6504  iota2df  6529  fnbrfvb  6943  fvelimab  6963  fvopab5  7029  fmptco  7128  fsng  7136  fressnfv  7159  fnpr2g  7213  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  25413  mbfinf  25414  degltlem1  25825  logltb  26344  cxple2  26441  rlimcnp  26706  rlimcnp2  26707  isppw2  26855  sqf11  26879  slerec  27557  tgjustc1  27993  tgjustc2  27994  f1otrgitv  28388  nbuhgr2vtx1edgb  28876  dfconngr1  29708  eupth2lem3lem6  29753  nmlno0i  30314  nmlno0  30315  blocn  30327  ubth  30393  hvsubeq0  30588  hvaddcan  30590  hvsubadd  30597  normsub0  30656  hlim2  30712  pjoc1  30954  pjoc2  30959  chne0  31014  chsscon3  31020  chlejb1  31032  chnle  31034  h1de2ci  31076  elspansn  31086  elspansn2  31087  cmbr3  31128  cmcm  31134  cmcm3  31135  pjch1  31190  pjch  31214  pj11  31234  pjnel  31246  eigorth  31358  elnlfn  31448  nmlnop0  31518  lnopeq  31529  lnopcon  31555  lnfncon  31576  pjdifnormi  31687  chrelat2  31890  cvexch  31894  mdsym  31932  eqelbid  31982  fmptcof2  32149  mgcoval  32423  mgcval  32424  mgccole1  32427  mgccole2  32428  mgcmnt1  32429  mgcmnt2  32430  mgccnv  32436  ist0cld  33111  zarclssn  33151  zart0  33157  signswch  33870  fnrelpredd  34390  cvmlift2lem12  34603  cvmlift2lem13  34604  satfv1lem  34651  satf0op  34666  fmlafvel  34674  abs2sqle  34963  abs2sqlt  34964  axextdist  35075  brimageg  35203  brdomaing  35211  brrangeg  35212  elhf2  35451  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  44182  fourierdlem31  45152  fourierdlem42  45163  fourierdlem54  45174  funressndmafv2rn  46229  dfatbrafv2b  46251  fnbrafv2b  46254  ichbidv  46419  ichnfim  46430  sprsymrelf  46461  sprsymrelfo  46463  isomuspgrlem2b  46795  isomuspgrlem2d  46797  line2ylem  47524  line2xlem  47526  mofeu  47601  catprslem  47717