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 279	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  1523  norass  1536  sbbib  2357  sb8eulem  2596  abbi  2808  cleqh  2860  clelab  2881  cleqf  2936  vtoclb  3507  vtoclbg  3512  ceqsexg  3588  elabgf  3610  elabgOLD  3613  reu6  3666  ru  3720  sbcbig  3775  unineq  4217  sbcnestgfw  4358  sbcnestgf  4363  preq12bg  4790  axrep1  5219  axrep4  5223  nalset  5246  opthg  5405  opelopabsb  5456  isso2i  5549  opeliunxp2  5760  resieq  5914  elimasngOLD  6008  dfpo2  6214  cbviotaw  6417  cbviota  6420  iota2df  6445  fnbrfvb  6854  fvelimab  6873  fvopab5  6939  fmptco  7033  fsng  7041  fressnfv  7064  fnpr2g  7118  isorel  7229  isocnv  7233  isocnv3  7235  isotr  7239  ovg  7469  caovcang  7505  caovordg  7511  caovord3d  7514  caovord  7515  orduninsuc  7722  opeliunxp2f  8057  brtpos  8082  dftpos4  8092  omopth  8523  ecopovsym  8639  xpf1o  8964  nneneq  9030  nneneqOLD  9042  ttrclselem2  9528  r1pwALT  9648  karden  9697  infxpenlem  9815  aceq0  9920  cflim2  10065  zfac  10262  ttukeylem1  10311  axextnd  10393  axrepndlem1  10394  axrepndlem2  10395  axrepnd  10396  axacndlem5  10413  zfcndrep  10416  zfcndac  10421  winalim  10497  gruina  10620  ltrnq  10781  ltsosr  10896  ltasr  10902  axpre-lttri  10967  axpre-ltadd  10969  nn0sub  12329  zextle  12439  zextlt  12440  xlesubadd  13043  sqeqor  13978  nn0opth2  14032  rexfiuz  15104  climshft  15330  rpnnen2lem10  15977  dvdsext  16075  ltoddhalfle  16115  halfleoddlt  16116  sumodd  16142  sadcadd  16210  dvdssq  16317  rpexp  16472  pcdvdsb  16615  imasleval  17297  isacs2  17407  acsfiel  17408  funcres2b  17657  pospropd  18090  isnsg  18828  nsgbi  18830  elnmz  18836  nmzbi  18837  oddvdsnn0  19197  odeq  19203  odmulg  19208  isslw  19258  slwispgp  19261  gsumval3lem2  19552  gsumcom2  19621  abveq0  20131  cnt0  22542  kqfvima  22926  kqt0lem  22932  isr0  22933  r0cld  22934  regr1lem2  22936  nrmr0reg  22945  isfildlem  23053  cnextfvval  23261  xmeteq0  23536  imasf1oxmet  23573  comet  23714  dscmet  23773  nrmmetd  23775  tngngp  23863  tngngp3  23865  mbfsup  24873  mbfinf  24874  degltlem1  25282  logltb  25800  cxple2  25897  rlimcnp  26160  rlimcnp2  26161  isppw2  26309  sqf11  26333  tgjustc1  26881  tgjustc2  26882  f1otrgitv  27276  nbuhgr2vtx1edgb  27764  dfconngr1  28597  eupth2lem3lem6  28642  nmlno0i  29201  nmlno0  29202  blocn  29214  ubth  29280  hvsubeq0  29475  hvaddcan  29477  hvsubadd  29484  normsub0  29543  hlim2  29599  pjoc1  29841  pjoc2  29846  chne0  29901  chsscon3  29907  chlejb1  29919  chnle  29921  h1de2ci  29963  elspansn  29973  elspansn2  29974  cmbr3  30015  cmcm  30021  cmcm3  30022  pjch1  30077  pjch  30101  pj11  30121  pjnel  30133  eigorth  30245  elnlfn  30335  nmlnop0  30405  lnopeq  30416  lnopcon  30442  lnfncon  30463  pjdifnormi  30574  chrelat2  30777  cvexch  30781  mdsym  30819  fmptcof2  31039  mgcoval  31309  mgcval  31310  mgccole1  31313  mgccole2  31314  mgcmnt1  31315  mgcmnt2  31316  mgccnv  31322  ist0cld  31828  zarclssn  31868  zart0  31874  signswch  32585  fnrelpredd  33106  cvmlift2lem12  33321  cvmlift2lem13  33322  satfv1lem  33369  satf0op  33384  fmlafvel  33392  abs2sqle  33683  abs2sqlt  33684  eqfunresadj  33780  axextdist  33820  xpord2pred  33837  xpord3pred  33843  slerec  34058  brimageg  34274  brdomaing  34282  brrangeg  34283  elhf2  34522  nn0prpwlem  34556  nn0prpw  34557  onsuct0  34675  bj-sbceqgALT  35131  bj-elabd2ALT  35157  bj-ru0  35175  eleq2w2ALT  35264  dfgcd3  35539  cbveud  35587  wl-3xorbi123d  35690  matunitlindf  35819  prdsbnd2  35997  isdrngo1  36158  eqrelf  36438  elsymrels5  36712  dfdisjs5  36865  eldisjs5  36879  lsatcmp  37059  llnexchb2  37925  lautset  38138  lautle  38140  sticksstones2  40145  dvdsexpnn0  40378  zindbi  40806  wepwsolem  40905  aomclem8  40924  ntrneik13  41746  ntrneix13  41747  ntrneik4w  41748  2sbc6g  42071  2sbc5g  42072  wessf1ornlem  42766  fourierdlem31  43728  fourierdlem42  43739  fourierdlem54  43750  funressndmafv2rn  44773  dfatbrafv2b  44795  fnbrafv2b  44798  ichbidv  44963  ichnfim  44974  sprsymrelf  45005  sprsymrelfo  45007  isomuspgrlem2b  45339  isomuspgrlem2d  45341  line2ylem  46155  line2xlem  46157  mofeu  46233  catprslem  46349