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 206

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 207

This theorem is referenced by:  bi2bian9  640  xorbi12d  1526  norass  1538  ru0  2130  sbbib  2361  sb8eulem  2593  abbib  2800  cleqh  2860  cleqf  2923  vtoclbg  3512  vtoclb  3523  ceqsexg  3608  elabgf  3630  reu6  3685  ruOLD  3740  sbcbig  3793  unineq  4238  sbcnestgfw  4371  sbcnestgf  4376  preq12bg  4805  axrep1  5218  axrep4OLD  5224  nalset  5251  opthg  5417  opelopabsb  5470  isso2i  5561  opeliunxp2  5778  resieq  5939  dfpo2  6243  cbviotaw  6444  cbviota  6446  iota2df  6468  fnbrfvb  6872  fvelimab  6894  fvopab5  6962  fmptco  7062  fsng  7070  fressnfv  7093  fnpr2g  7144  isorel  7260  isocnv  7264  isocnv3  7266  isotr  7270  eqfunresadj  7294  ovg  7511  caovcang  7547  caovordg  7553  caovord3d  7556  caovord  7557  caofidlcan  7648  orduninsuc  7773  xpord2pred  8075  xpord3pred  8082  opeliunxp2f  8140  brtpos  8165  dftpos4  8175  omopth  8577  ecopovsym  8743  xpf1o  9052  nneneq  9115  ttrclselem2  9616  r1pwALT  9736  karden  9785  infxpenlem  9901  aceq0  10006  cflim2  10151  zfac  10348  ttukeylem1  10397  axextnd  10479  axrepndlem1  10480  axrepndlem2  10481  axrepnd  10482  axacndlem5  10499  zfcndrep  10502  zfcndac  10507  winalim  10583  gruina  10706  ltrnq  10867  ltsosr  10982  ltasr  10988  axpre-lttri  11053  axpre-ltadd  11055  nn0sub  12428  zextle  12543  zextlt  12544  xlesubadd  13159  sqeqor  14120  nn0opth2  14176  rexfiuz  15252  climshft  15480  rpnnen2lem10  16129  dvdsext  16229  ltoddhalfle  16269  halfleoddlt  16270  sumodd  16296  sadcadd  16366  dvdssq  16475  rpexp  16630  pcdvdsb  16778  imasleval  17442  isacs2  17556  acsfiel  17557  funcres2b  17801  pospropd  18228  isnsg  19065  nsgbi  19067  elnmz  19073  nmzbi  19074  oddvdsnn0  19454  odeq  19460  odmulg  19466  isslw  19518  slwispgp  19521  gsumval3lem2  19816  gsumcom2  19885  abveq0  20731  cnt0  23259  kqfvima  23643  kqt0lem  23649  isr0  23650  r0cld  23651  regr1lem2  23653  nrmr0reg  23662  isfildlem  23770  cnextfvval  23978  xmeteq0  24251  imasf1oxmet  24288  comet  24426  dscmet  24485  nrmmetd  24487  tngngp  24567  tngngp3  24569  mbfsup  25590  mbfinf  25591  degltlem1  26002  logltb  26534  cxple2  26631  rlimcnp  26900  rlimcnp2  26901  isppw2  27050  sqf11  27074  slerec  27758  tgjustc1  28451  tgjustc2  28452  f1otrgitv  28846  nbuhgr2vtx1edgb  29328  dfconngr1  30163  eupth2lem3lem6  30208  nmlno0i  30769  nmlno0  30770  blocn  30782  ubth  30848  hvsubeq0  31043  hvaddcan  31045  hvsubadd  31052  normsub0  31111  hlim2  31167  pjoc1  31409  pjoc2  31414  chne0  31469  chsscon3  31475  chlejb1  31487  chnle  31489  h1de2ci  31531  elspansn  31541  elspansn2  31542  cmbr3  31583  cmcm  31589  cmcm3  31590  pjch1  31645  pjch  31669  pj11  31689  pjnel  31701  eigorth  31813  elnlfn  31903  nmlnop0  31973  lnopeq  31984  lnopcon  32010  lnfncon  32031  pjdifnormi  32142  chrelat2  32345  cvexch  32349  mdsym  32387  eqelbid  32449  fmptcof2  32634  mgcoval  32962  mgcval  32963  mgccole1  32966  mgccole2  32967  mgcmnt1  32968  mgcmnt2  32969  mgccnv  32975  unitprodclb  33349  ist0cld  33841  zarclssn  33881  zart0  33887  signswch  34569  fnrelpredd  35097  r1omhfbregs  35121  cvmlift2lem12  35346  cvmlift2lem13  35347  satfv1lem  35394  satf0op  35409  fmlafvel  35417  abs2sqle  35712  abs2sqlt  35713  axextdist  35832  brimageg  35960  brdomaing  35968  brrangeg  35969  elhf2  36208  nn0prpwlem  36355  nn0prpw  36356  onsuct0  36474  bj-sbceqgALT  36935  bj-elabd2ALT  36958  eleq2w2ALT  37080  dfgcd3  37357  cbveud  37405  wl-3xorbi123d  37508  matunitlindf  37657  prdsbnd2  37834  isdrngo1  37995  eqrelf  38289  elsymrels5  38592  dfdisjs5  38749  eldisjs5  38763  mpets2  38878  pets  38889  lsatcmp  39041  llnexchb2  39907  lautset  40120  lautle  40122  sticksstones2  42179  aks6d1c7  42216  dvdsexpnn0  42366  eu6w  42708  abbibw  42709  zindbi  42978  wepwsolem  43074  aomclem8  43093  onsupmaxb  43271  oaordnr  43328  omnord1  43337  oenord1  43348  ntrneik13  44130  ntrneix13  44131  ntrneik4w  44132  2sbc6g  44447  2sbc5g  44448  modelaxreplem3  45012  wessf1ornlem  45221  fourierdlem31  46175  fourierdlem42  46186  fourierdlem54  46197  funressndmafv2rn  47253  dfatbrafv2b  47275  fnbrafv2b  47278  ichbidv  47483  ichnfim  47494  sprsymrelf  47525  sprsymrelfo  47527  isuspgrimlem  47925  line2ylem  48782  line2xlem  48784  mofeu  48878  tposres0  48907  catprslem  49041