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  2132  sbbib  2365  sb8eulem  2598  abbib  2805  cleqh  2865  cleqf  2927  vtoclbg  3514  vtoclb  3524  ceqsexg  3607  elabgf  3629  reu6  3684  ruOLD  3739  sbcbig  3792  unineq  4240  sbcnestgfw  4373  sbcnestgf  4378  preq12bg  4809  axrep1  5225  axrep4OLD  5231  nalset  5258  opthg  5425  opelopabsb  5478  isso2i  5569  opeliunxp2  5787  resieq  5949  dfpo2  6254  cbviotaw  6455  cbviota  6457  iota2df  6479  fnbrfvb  6884  fvelimab  6906  fvopab5  6974  fmptco  7074  fsng  7082  fressnfv  7105  fnpr2g  7156  isorel  7272  isocnv  7276  isocnv3  7278  isotr  7282  eqfunresadj  7306  ovg  7523  caovcang  7559  caovordg  7565  caovord3d  7568  caovord  7569  caofidlcan  7660  orduninsuc  7785  xpord2pred  8087  xpord3pred  8094  opeliunxp2f  8152  brtpos  8177  dftpos4  8187  omopth  8590  ecopovsym  8756  xpf1o  9067  nneneq  9130  ttrclselem2  9635  r1pwALT  9758  karden  9807  infxpenlem  9923  aceq0  10028  cflim2  10173  zfac  10370  ttukeylem1  10419  axextnd  10502  axrepndlem1  10503  axrepndlem2  10504  axrepnd  10505  axacndlem5  10522  zfcndrep  10525  zfcndac  10530  winalim  10606  gruina  10729  ltrnq  10890  ltsosr  11005  ltasr  11011  axpre-lttri  11076  axpre-ltadd  11078  nn0sub  12451  zextle  12565  zextlt  12566  xlesubadd  13178  sqeqor  14139  nn0opth2  14195  rexfiuz  15271  climshft  15499  rpnnen2lem10  16148  dvdsext  16248  ltoddhalfle  16288  halfleoddlt  16289  sumodd  16315  sadcadd  16385  dvdssq  16494  rpexp  16649  pcdvdsb  16797  imasleval  17462  isacs2  17576  acsfiel  17577  funcres2b  17821  pospropd  18248  isnsg  19084  nsgbi  19086  elnmz  19092  nmzbi  19093  oddvdsnn0  19473  odeq  19479  odmulg  19485  isslw  19537  slwispgp  19540  gsumval3lem2  19835  gsumcom2  19904  abveq0  20751  cnt0  23290  kqfvima  23674  kqt0lem  23680  isr0  23681  r0cld  23682  regr1lem2  23684  nrmr0reg  23693  isfildlem  23801  cnextfvval  24009  xmeteq0  24282  imasf1oxmet  24319  comet  24457  dscmet  24516  nrmmetd  24518  tngngp  24598  tngngp3  24600  mbfsup  25621  mbfinf  25622  degltlem1  26033  logltb  26565  cxple2  26662  rlimcnp  26931  rlimcnp2  26932  isppw2  27081  sqf11  27105  lesrec  27795  tgjustc1  28547  tgjustc2  28548  f1otrgitv  28942  nbuhgr2vtx1edgb  29425  dfconngr1  30263  eupth2lem3lem6  30308  nmlno0i  30869  nmlno0  30870  blocn  30882  ubth  30948  hvsubeq0  31143  hvaddcan  31145  hvsubadd  31152  normsub0  31211  hlim2  31267  pjoc1  31509  pjoc2  31514  chne0  31569  chsscon3  31575  chlejb1  31587  chnle  31589  h1de2ci  31631  elspansn  31641  elspansn2  31642  cmbr3  31683  cmcm  31689  cmcm3  31690  pjch1  31745  pjch  31769  pj11  31789  pjnel  31801  eigorth  31913  elnlfn  32003  nmlnop0  32073  lnopeq  32084  lnopcon  32110  lnfncon  32131  pjdifnormi  32242  chrelat2  32445  cvexch  32449  mdsym  32487  eqelbid  32549  fmptcof2  32735  mgcoval  33068  mgcval  33069  mgccole1  33072  mgccole2  33073  mgcmnt1  33074  mgcmnt2  33075  mgccnv  33081  domnprodeq0  33358  unitprodclb  33470  ist0cld  33990  zarclssn  34030  zart0  34036  signswch  34718  fnrelpredd  35247  r1omhfb  35268  r1omhfbregs  35293  cvmlift2lem12  35508  cvmlift2lem13  35509  satfv1lem  35556  satf0op  35571  fmlafvel  35579  abs2sqle  35874  abs2sqlt  35875  axextdist  35991  brimageg  36119  brdomaing  36127  brrangeg  36128  elhf2  36369  nn0prpwlem  36516  nn0prpw  36517  onsuct0  36635  bj-sbceqgALT  37103  bj-elabd2ALT  37126  eleq2w2ALT  37248  dfgcd3  37525  cbveud  37573  wl-3xorbi123d  37676  matunitlindf  37815  prdsbnd2  37992  isdrngo1  38153  eqrelf  38449  elsymrels5  38809  dfdisjs5  38967  eldisjs5  38981  mpets2  39096  pets  39107  lsatcmp  39259  llnexchb2  40125  lautset  40338  lautle  40340  sticksstones2  42397  aks6d1c7  42434  dvdsexpnn0  42585  eu6w  42915  abbibw  42916  zindbi  43184  wepwsolem  43280  aomclem8  43299  onsupmaxb  43477  oaordnr  43534  omnord1  43543  oenord1  43554  ntrneik13  44335  ntrneix13  44336  ntrneik4w  44337  2sbc6g  44652  2sbc5g  44653  modelaxreplem3  45217  wessf1ornlem  45425  fourierdlem31  46378  fourierdlem42  46389  fourierdlem54  46400  funressndmafv2rn  47465  dfatbrafv2b  47487  fnbrafv2b  47490  ichbidv  47695  ichnfim  47706  sprsymrelf  47737  sprsymrelfo  47739  isuspgrimlem  48137  line2ylem  48993  line2xlem  48995  mofeu  49089  tposres0  49118  catprslem  49251