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  639  xorbi12d  1522  norass  1534  ru0  2127  sbbib  2367  sb8eulem  2601  abbib  2814  cleqh  2874  cleqf  2940  vtoclbg  3569  vtoclb  3580  ceqsexg  3666  elabgf  3688  elabgOLD  3691  reu6  3748  ruOLD  3803  sbcbig  3859  unineq  4307  sbcnestgfw  4444  sbcnestgf  4449  preq12bg  4878  axrep1  5304  axrep4  5308  nalset  5331  opthg  5497  opelopabsb  5549  isso2i  5644  opeliunxp2  5863  resieq  6020  elimasngOLD  6120  dfpo2  6327  cbviotaw  6532  cbviota  6535  iota2df  6560  fnbrfvb  6973  fvelimab  6994  fvopab5  7062  fmptco  7163  fsng  7171  fressnfv  7194  fnpr2g  7247  isorel  7362  isocnv  7366  isocnv3  7368  isotr  7372  eqfunresadj  7396  ovg  7615  caovcang  7651  caovordg  7657  caovord3d  7660  caovord  7661  orduninsuc  7880  xpord2pred  8186  xpord3pred  8193  opeliunxp2f  8251  brtpos  8276  dftpos4  8286  omopth  8718  ecopovsym  8877  xpf1o  9205  nneneq  9272  nneneqOLD  9284  ttrclselem2  9795  r1pwALT  9915  karden  9964  infxpenlem  10082  aceq0  10187  cflim2  10332  zfac  10529  ttukeylem1  10578  axextnd  10660  axrepndlem1  10661  axrepndlem2  10662  axrepnd  10663  axacndlem5  10680  zfcndrep  10683  zfcndac  10688  winalim  10764  gruina  10887  ltrnq  11048  ltsosr  11163  ltasr  11169  axpre-lttri  11234  axpre-ltadd  11236  nn0sub  12603  zextle  12716  zextlt  12717  xlesubadd  13325  sqeqor  14265  nn0opth2  14321  rexfiuz  15396  climshft  15622  rpnnen2lem10  16271  dvdsext  16369  ltoddhalfle  16409  halfleoddlt  16410  sumodd  16436  sadcadd  16504  dvdssq  16614  rpexp  16769  pcdvdsb  16916  imasleval  17601  isacs2  17711  acsfiel  17712  funcres2b  17961  pospropd  18397  isnsg  19195  nsgbi  19197  elnmz  19203  nmzbi  19204  oddvdsnn0  19586  odeq  19592  odmulg  19598  isslw  19650  slwispgp  19653  gsumval3lem2  19948  gsumcom2  20017  abveq0  20841  cnt0  23375  kqfvima  23759  kqt0lem  23765  isr0  23766  r0cld  23767  regr1lem2  23769  nrmr0reg  23778  isfildlem  23886  cnextfvval  24094  xmeteq0  24369  imasf1oxmet  24406  comet  24547  dscmet  24606  nrmmetd  24608  tngngp  24696  tngngp3  24698  mbfsup  25718  mbfinf  25719  degltlem1  26131  logltb  26660  cxple2  26757  rlimcnp  27026  rlimcnp2  27027  isppw2  27176  sqf11  27200  slerec  27882  tgjustc1  28501  tgjustc2  28502  f1otrgitv  28896  nbuhgr2vtx1edgb  29387  dfconngr1  30220  eupth2lem3lem6  30265  nmlno0i  30826  nmlno0  30827  blocn  30839  ubth  30905  hvsubeq0  31100  hvaddcan  31102  hvsubadd  31109  normsub0  31168  hlim2  31224  pjoc1  31466  pjoc2  31471  chne0  31526  chsscon3  31532  chlejb1  31544  chnle  31546  h1de2ci  31588  elspansn  31598  elspansn2  31599  cmbr3  31640  cmcm  31646  cmcm3  31647  pjch1  31702  pjch  31726  pj11  31746  pjnel  31758  eigorth  31870  elnlfn  31960  nmlnop0  32030  lnopeq  32041  lnopcon  32067  lnfncon  32088  pjdifnormi  32199  chrelat2  32402  cvexch  32406  mdsym  32444  eqelbid  32503  fmptcof2  32675  mgcoval  32959  mgcval  32960  mgccole1  32963  mgccole2  32964  mgcmnt1  32965  mgcmnt2  32966  mgccnv  32972  unitprodclb  33382  ist0cld  33779  zarclssn  33819  zart0  33825  signswch  34538  fnrelpredd  35065  cvmlift2lem12  35282  cvmlift2lem13  35283  satfv1lem  35330  satf0op  35345  fmlafvel  35353  abs2sqle  35648  abs2sqlt  35649  axextdist  35763  brimageg  35891  brdomaing  35899  brrangeg  35900  elhf2  36139  nn0prpwlem  36288  nn0prpw  36289  onsuct0  36407  bj-sbceqgALT  36868  bj-elabd2ALT  36891  eleq2w2ALT  37013  dfgcd3  37290  cbveud  37338  wl-3xorbi123d  37441  matunitlindf  37578  prdsbnd2  37755  isdrngo1  37916  eqrelf  38211  elsymrels5  38512  dfdisjs5  38668  eldisjs5  38682  mpets2  38797  pets  38808  lsatcmp  38959  llnexchb2  39826  lautset  40039  lautle  40041  sticksstones2  42104  aks6d1c7  42141  dvdsexpnn0  42321  eu6w  42631  abbibw  42632  zindbi  42903  wepwsolem  42999  aomclem8  43018  onsupmaxb  43200  oaordnr  43258  omnord1  43267  oenord1  43278  ntrneik13  44060  ntrneix13  44061  ntrneik4w  44062  2sbc6g  44384  2sbc5g  44385  wessf1ornlem  45092  fourierdlem31  46059  fourierdlem42  46070  fourierdlem54  46081  funressndmafv2rn  47138  dfatbrafv2b  47160  fnbrafv2b  47163  ichbidv  47327  ichnfim  47338  sprsymrelf  47369  sprsymrelfo  47371  isuspgrimlem  47758  line2ylem  48485  line2xlem  48487  mofeu  48561  catprslem  48677