Theorem bibi12d 348

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bi2bian9  651  xorbi12d  1548  norass  1560  ru0  2164  sbbib  2395  sb8eulem  2628  abbib  2834  cleqh  2894  cleqf  2955  vtoclbg  3527  vtoclb  3536  ceqsexg  3615  elabgf  3636  reu6  3692  sbcbig  3798  unineq  4243  sbcnestgfw  4378  sbcnestgf  4383  preq12bg  4813  axrep1  5232  axrep4OLD  5238  nalsetOLD  5269  opthg  5449  opelopabsb  5504  isso2i  5596  opeliunxp2  5814  resieq  5979  dfpo2  6286  cbviotaw  6488  cbviota  6490  iota2df  6512  fnbrfvb  6921  fvelimab  6943  fvopab5  7013  fmptco  7115  fsng  7123  fressnfv  7147  fnpr2g  7198  isorel  7314  isocnv  7318  isocnv3  7320  isotr  7324  eqfunresadj  7348  ovg  7565  caovcang  7601  caovordg  7607  caovord3d  7610  caovord  7611  caofidlcan  7702  orduninsuc  7827  xpord2pred  8129  xpord3pred  8136  opeliunxp2f  8194  brtpos  8219  dftpos4  8229  omopth  8636  ecopovsym  8805  xpf1o  9115  nneneq  9178  ttrclselem2  9683  r1pwALT  9806  karden  9869  infxpenlem  9985  aceq0  10090  cflim2  10235  zfac  10432  ttukeylem1  10481  axextnd  10564  axrepndlem1  10565  axrepndlem2  10566  axrepnd  10567  axacndlem5  10584  zfcndrep  10587  zfcndac  10592  winalim  10668  gruina  10791  ltrnq  10952  ltsosr  11067  ltasr  11073  axpre-lttri  11138  axpre-ltadd  11140  nn0sub  12542  zextle  12657  zextlt  12658  xlesubadd  13277  sqeqor  14240  nn0opth2  14296  rexfiuz  15387  climshft  15615  rpnnen2lem10  16267  dvdsext  16367  ltoddhalfle  16407  halfleoddlt  16408  sumodd  16434  sadcadd  16504  dvdssq  16613  rpexp  16769  pcdvdsb  16917  imasleval  17583  isacs2  17697  acsfiel  17698  funcres2b  17942  pospropd  18369  isnsg  19209  nsgbi  19211  elnmz  19217  nmzbi  19218  oddvdsnn0  19602  odeq  19608  odmulg  19614  isslw  19666  slwispgp  19669  gsumval3lem2  19964  gsumcom2  20033  abveq0  20887  cnt0  23460  kqfvima  23844  kqt0lem  23850  isr0  23851  r0cld  23852  regr1lem2  23854  nrmr0reg  23863  isfildlem  23971  cnextfvval  24179  xmeteq0  24452  imasf1oxmet  24489  comet  24627  dscmet  24686  nrmmetd  24688  tngngp  24768  tngngp3  24770  mbfsup  25780  mbfinf  25781  degltlem1  26186  logltb  26719  cxple2  26816  rlimcnp  27084  rlimcnp2  27085  isppw2  27233  sqf11  27257  lesrec  27946  tgjustc1  28698  tgjustc2  28699  f1otrgitv  29124  nbuhgr2vtx1edgb  29607  dfconngr1  30444  eupth2lem3lem6  30489  nmlno0i  31051  nmlno0  31052  blocn  31064  ubth  31130  hvsubeq0  31325  hvaddcan  31327  hvsubadd  31334  normsub0  31393  hlim2  31449  pjoc1  31691  pjoc2  31696  chne0  31751  chsscon3  31757  chlejb1  31769  chnle  31771  h1de2ci  31813  elspansn  31823  elspansn2  31824  cmbr3  31865  cmcm  31871  cmcm3  31872  pjch1  31927  pjch  31951  pj11  31971  pjnel  31983  eigorth  32095  elnlfn  32185  nmlnop0  32255  lnopeq  32266  lnopcon  32292  lnfncon  32313  pjdifnormi  32424  chrelat2  32627  cvexch  32631  mdsym  32669  eqelbid  32727  fmptcof2  32910  mgcoval  33214  mgcval  33215  mgccole1  33218  mgccole2  33219  mgcmnt1  33220  mgcmnt2  33221  mgccnv  33227  domnprodeq0  33507  unitprodclb  33613  ist0cld  34135  zarclssn  34175  zart0  34181  signswch  34860  fnrelpredd  35392  r1omhfb  35415  r1omhfbregs  35440  axsepg2  35443  axsepg4  35446  cvmlift2lem12  35672  cvmlift2lem13  35673  satfv1lem  35720  satf0op  35735  fmlafvel  35743  abs2sqle  36038  abs2sqlt  36039  axextdist  36155  brimageg  36283  brdomaing  36291  brrangeg  36292  elhf2  36533  nn0prpwlem  36690  nn0prpw  36691  onsuct0  36809  ttcwf2  36893  bj-sbceqgALT  37394  bj-elabd2ALT  37417  eleq2w2ALT  37539  bj-axseprep  37566  dfgcd3  37823  cbveud  37873  wl-3xorbi123d  37976  wl-dfcleq  38015  matunitlindf  38124  prdsbnd2  38301  isdrngo1  38462  eqrelf  38764  elsymrels5  39146  dfdisjs5  39303  eldisjs5  39329  mpets2  39461  pets  39472  lsatcmp  39634  llnexchb2  40500  lautset  40713  lautle  40715  sticksstones2  42771  aks6d1c7  42808  dvdsexpnn0  42950  eu6w  43265  abbibw  43266  zindbi  43530  wepwsolem  43626  aomclem8  43645  onsupmaxb  43823  oaordnr  43880  omnord1  43889  oenord1  43900  ntrneik13  44681  ntrneix13  44682  ntrneik4w  44683  2sbc6g  44984  2sbc5g  44985  modelaxreplem3  45548  wessf1ornlem  45762  fourierdlem31  46711  fourierdlem42  46722  fourierdlem54  46733  funressndmafv2rn  47816  dfatbrafv2b  47838  fnbrafv2b  47841  ichbidv  48058  ichnfim  48069  sprsymrelf  48100  sprsymrelfo  48102  isuspgrimlem  48516  line2ylem  49383  line2xlem  49385  mofeu  49478  tposres0  49507  catprslem  49640