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  641  xorbi12d  1527  norass  1539  ru0  2133  sbbib  2366  sb8eulem  2599  abbib  2806  cleqh  2866  cleqf  2928  vtoclbg  3516  vtoclb  3526  ceqsexg  3609  elabgf  3631  reu6  3686  ruOLD  3741  sbcbig  3794  unineq  4242  sbcnestgfw  4375  sbcnestgf  4380  preq12bg  4811  axrep1  5227  axrep4OLD  5233  nalset  5260  opthg  5433  opelopabsb  5486  isso2i  5577  opeliunxp2  5795  resieq  5957  dfpo2  6262  cbviotaw  6463  cbviota  6465  iota2df  6487  fnbrfvb  6892  fvelimab  6914  fvopab5  6983  fmptco  7084  fsng  7092  fressnfv  7115  fnpr2g  7166  isorel  7282  isocnv  7286  isocnv3  7288  isotr  7292  eqfunresadj  7316  ovg  7533  caovcang  7569  caovordg  7575  caovord3d  7578  caovord  7579  caofidlcan  7670  orduninsuc  7795  xpord2pred  8097  xpord3pred  8104  opeliunxp2f  8162  brtpos  8187  dftpos4  8197  omopth  8600  ecopovsym  8768  xpf1o  9079  nneneq  9142  ttrclselem2  9647  r1pwALT  9770  karden  9819  infxpenlem  9935  aceq0  10040  cflim2  10185  zfac  10382  ttukeylem1  10431  axextnd  10514  axrepndlem1  10515  axrepndlem2  10516  axrepnd  10517  axacndlem5  10534  zfcndrep  10537  zfcndac  10542  winalim  10618  gruina  10741  ltrnq  10902  ltsosr  11017  ltasr  11023  axpre-lttri  11088  axpre-ltadd  11090  nn0sub  12463  zextle  12577  zextlt  12578  xlesubadd  13190  sqeqor  14151  nn0opth2  14207  rexfiuz  15283  climshft  15511  rpnnen2lem10  16160  dvdsext  16260  ltoddhalfle  16300  halfleoddlt  16301  sumodd  16327  sadcadd  16397  dvdssq  16506  rpexp  16661  pcdvdsb  16809  imasleval  17474  isacs2  17588  acsfiel  17589  funcres2b  17833  pospropd  18260  isnsg  19096  nsgbi  19098  elnmz  19104  nmzbi  19105  oddvdsnn0  19485  odeq  19491  odmulg  19497  isslw  19549  slwispgp  19552  gsumval3lem2  19847  gsumcom2  19916  abveq0  20763  cnt0  23302  kqfvima  23686  kqt0lem  23692  isr0  23693  r0cld  23694  regr1lem2  23696  nrmr0reg  23705  isfildlem  23813  cnextfvval  24021  xmeteq0  24294  imasf1oxmet  24331  comet  24469  dscmet  24528  nrmmetd  24530  tngngp  24610  tngngp3  24612  mbfsup  25633  mbfinf  25634  degltlem1  26045  logltb  26577  cxple2  26674  rlimcnp  26943  rlimcnp2  26944  isppw2  27093  sqf11  27117  lesrec  27807  tgjustc1  28559  tgjustc2  28560  f1otrgitv  28954  nbuhgr2vtx1edgb  29437  dfconngr1  30275  eupth2lem3lem6  30320  nmlno0i  30881  nmlno0  30882  blocn  30894  ubth  30960  hvsubeq0  31155  hvaddcan  31157  hvsubadd  31164  normsub0  31223  hlim2  31279  pjoc1  31521  pjoc2  31526  chne0  31581  chsscon3  31587  chlejb1  31599  chnle  31601  h1de2ci  31643  elspansn  31653  elspansn2  31654  cmbr3  31695  cmcm  31701  cmcm3  31702  pjch1  31757  pjch  31781  pj11  31801  pjnel  31813  eigorth  31925  elnlfn  32015  nmlnop0  32085  lnopeq  32096  lnopcon  32122  lnfncon  32143  pjdifnormi  32254  chrelat2  32457  cvexch  32461  mdsym  32499  eqelbid  32560  fmptcof2  32746  mgcoval  33078  mgcval  33079  mgccole1  33082  mgccole2  33083  mgcmnt1  33084  mgcmnt2  33085  mgccnv  33091  domnprodeq0  33369  unitprodclb  33481  ist0cld  34010  zarclssn  34050  zart0  34056  signswch  34738  fnrelpredd  35266  r1omhfb  35287  r1omhfbregs  35312  cvmlift2lem12  35527  cvmlift2lem13  35528  satfv1lem  35575  satf0op  35590  fmlafvel  35598  abs2sqle  35893  abs2sqlt  35894  axextdist  36010  brimageg  36138  brdomaing  36146  brrangeg  36147  elhf2  36388  nn0prpwlem  36535  nn0prpw  36536  onsuct0  36654  bj-sbceqgALT  37144  bj-elabd2ALT  37167  eleq2w2ALT  37289  bj-axseprep  37316  dfgcd3  37573  cbveud  37621  wl-3xorbi123d  37724  matunitlindf  37863  prdsbnd2  38040  isdrngo1  38201  eqrelf  38503  elsymrels5  38885  dfdisjs5  39042  eldisjs5  39068  mpets2  39200  pets  39211  lsatcmp  39373  llnexchb2  40239  lautset  40452  lautle  40454  sticksstones2  42511  aks6d1c7  42548  dvdsexpnn0  42698  eu6w  43028  abbibw  43029  zindbi  43297  wepwsolem  43393  aomclem8  43412  onsupmaxb  43590  oaordnr  43647  omnord1  43656  oenord1  43667  ntrneik13  44448  ntrneix13  44449  ntrneik4w  44450  2sbc6g  44765  2sbc5g  44766  modelaxreplem3  45330  wessf1ornlem  45538  fourierdlem31  46490  fourierdlem42  46501  fourierdlem54  46512  funressndmafv2rn  47577  dfatbrafv2b  47599  fnbrafv2b  47602  ichbidv  47807  ichnfim  47818  sprsymrelf  47849  sprsymrelfo  47851  isuspgrimlem  48249  line2ylem  49105  line2xlem  49107  mofeu  49201  tposres0  49230  catprslem  49363