Theorem bibi12d 346

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 344	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 343	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 280	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bi2bian9  646  xorbi12d  1532  norass  1544  ru0  2138  sbbib  2369  sb8eulem  2602  abbib  2809  cleqh  2869  cleqf  2930  vtoclbg  3505  vtoclb  3515  ceqsexg  3598  elabgf  3619  reu6  3674  ruOLD  3729  sbcbig  3781  unineq  4223  sbcnestgfw  4356  sbcnestgf  4361  preq12bg  4791  axrep1  5207  axrep4OLD  5213  nalsetOLD  5244  opthg  5424  opelopabsb  5479  isso2i  5570  opeliunxp2  5787  resieq  5949  dfpo2  6254  cbviotaw  6455  cbviota  6457  iota2df  6479  fnbrfvb  6884  fvelimab  6906  fvopab5  6976  fmptco  7078  fsng  7086  fressnfv  7110  fnpr2g  7161  isorel  7277  isocnv  7281  isocnv3  7283  isotr  7287  eqfunresadj  7311  ovg  7528  caovcang  7564  caovordg  7570  caovord3d  7573  caovord  7574  caofidlcan  7665  orduninsuc  7790  xpord2pred  8092  xpord3pred  8099  opeliunxp2f  8157  brtpos  8182  dftpos4  8192  omopth  8595  ecopovsym  8763  xpf1o  9074  nneneq  9137  ttrclselem2  9645  r1pwALT  9768  karden  9817  infxpenlem  9933  aceq0  10038  cflim2  10183  zfac  10380  ttukeylem1  10429  axextnd  10512  axrepndlem1  10513  axrepndlem2  10514  axrepnd  10515  axacndlem5  10532  zfcndrep  10535  zfcndac  10540  winalim  10616  gruina  10739  ltrnq  10900  ltsosr  11015  ltasr  11021  axpre-lttri  11086  axpre-ltadd  11088  nn0sub  12485  zextle  12600  zextlt  12601  xlesubadd  13213  sqeqor  14176  nn0opth2  14232  rexfiuz  15308  climshft  15536  rpnnen2lem10  16188  dvdsext  16288  ltoddhalfle  16328  halfleoddlt  16329  sumodd  16355  sadcadd  16425  dvdssq  16534  rpexp  16690  pcdvdsb  16838  imasleval  17503  isacs2  17617  acsfiel  17618  funcres2b  17862  pospropd  18289  isnsg  19128  nsgbi  19130  elnmz  19136  nmzbi  19137  oddvdsnn0  19517  odeq  19523  odmulg  19529  isslw  19581  slwispgp  19584  gsumval3lem2  19879  gsumcom2  19948  abveq0  20797  cnt0  23336  kqfvima  23720  kqt0lem  23726  isr0  23727  r0cld  23728  regr1lem2  23730  nrmr0reg  23739  isfildlem  23847  cnextfvval  24055  xmeteq0  24328  imasf1oxmet  24365  comet  24503  dscmet  24562  nrmmetd  24564  tngngp  24644  tngngp3  24646  mbfsup  25656  mbfinf  25657  degltlem1  26062  logltb  26589  cxple2  26686  rlimcnp  26954  rlimcnp2  26955  isppw2  27103  sqf11  27127  lesrec  27816  tgjustc1  28568  tgjustc2  28569  f1otrgitv  28963  nbuhgr2vtx1edgb  29446  dfconngr1  30283  eupth2lem3lem6  30328  nmlno0i  30890  nmlno0  30891  blocn  30903  ubth  30969  hvsubeq0  31164  hvaddcan  31166  hvsubadd  31173  normsub0  31232  hlim2  31288  pjoc1  31530  pjoc2  31535  chne0  31590  chsscon3  31596  chlejb1  31608  chnle  31610  h1de2ci  31652  elspansn  31662  elspansn2  31663  cmbr3  31704  cmcm  31710  cmcm3  31711  pjch1  31766  pjch  31790  pj11  31810  pjnel  31822  eigorth  31934  elnlfn  32024  nmlnop0  32094  lnopeq  32105  lnopcon  32131  lnfncon  32152  pjdifnormi  32263  chrelat2  32466  cvexch  32470  mdsym  32508  eqelbid  32569  fmptcof2  32756  mgcoval  33072  mgcval  33073  mgccole1  33076  mgccole2  33077  mgcmnt1  33078  mgcmnt2  33079  mgccnv  33085  domnprodeq0  33364  unitprodclb  33479  ist0cld  34024  zarclssn  34064  zart0  34070  signswch  34752  fnrelpredd  35279  r1omhfb  35300  r1omhfbregs  35325  axsepg2  35328  axsepg4  35331  cvmlift2lem12  35549  cvmlift2lem13  35550  satfv1lem  35597  satf0op  35612  fmlafvel  35620  abs2sqle  35915  abs2sqlt  35916  axextdist  36032  brimageg  36160  brdomaing  36168  brrangeg  36169  elhf2  36410  nn0prpwlem  36557  nn0prpw  36558  onsuct0  36676  ttcwf2  36760  bj-sbceqgALT  37262  bj-elabd2ALT  37285  eleq2w2ALT  37407  bj-axseprep  37434  dfgcd3  37691  cbveud  37741  wl-3xorbi123d  37844  wl-dfcleq  37883  matunitlindf  37992  prdsbnd2  38169  isdrngo1  38330  eqrelf  38632  elsymrels5  39014  dfdisjs5  39171  eldisjs5  39197  mpets2  39329  pets  39340  lsatcmp  39502  llnexchb2  40368  lautset  40581  lautle  40583  sticksstones2  42639  aks6d1c7  42676  dvdsexpnn0  42818  eu6w  43133  abbibw  43134  zindbi  43398  wepwsolem  43494  aomclem8  43513  onsupmaxb  43691  oaordnr  43748  omnord1  43757  oenord1  43768  ntrneik13  44549  ntrneix13  44550  ntrneik4w  44551  2sbc6g  44866  2sbc5g  44867  modelaxreplem3  45431  wessf1ornlem  45639  fourierdlem31  46588  fourierdlem42  46599  fourierdlem54  46610  funressndmafv2rn  47693  dfatbrafv2b  47715  fnbrafv2b  47718  ichbidv  47935  ichnfim  47946  sprsymrelf  47977  sprsymrelfo  47979  isuspgrimlem  48393  line2ylem  49249  line2xlem  49251  mofeu  49345  tposres0  49374  catprslem  49507