Theorem bibi12d 347

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bi2bian9  649  xorbi12d  1544  norass  1556  ru0  2160  sbbib  2391  sb8eulem  2624  abbib  2830  cleqh  2890  cleqf  2951  vtoclbg  3523  vtoclb  3533  ceqsexg  3612  elabgf  3633  reu6  3688  ruOLD  3743  sbcbig  3795  unineq  4240  sbcnestgfw  4374  sbcnestgf  4379  preq12bg  4810  axrep1  5227  axrep4OLD  5233  nalsetOLD  5264  opthg  5444  opelopabsb  5499  isso2i  5590  opeliunxp2  5808  resieq  5974  dfpo2  6279  cbviotaw  6480  cbviota  6482  iota2df  6504  fnbrfvb  6913  fvelimab  6935  fvopab5  7005  fmptco  7107  fsng  7115  fressnfv  7139  fnpr2g  7190  isorel  7306  isocnv  7310  isocnv3  7312  isotr  7316  eqfunresadj  7340  ovg  7557  caovcang  7593  caovordg  7599  caovord3d  7602  caovord  7603  caofidlcan  7694  orduninsuc  7819  xpord2pred  8120  xpord3pred  8127  opeliunxp2f  8185  brtpos  8210  dftpos4  8220  omopth  8627  ecopovsym  8796  xpf1o  9107  nneneq  9170  ttrclselem2  9678  r1pwALT  9801  karden  9850  infxpenlem  9966  aceq0  10071  cflim2  10217  zfac  10414  ttukeylem1  10463  axextnd  10546  axrepndlem1  10547  axrepndlem2  10548  axrepnd  10549  axacndlem5  10566  zfcndrep  10569  zfcndac  10574  winalim  10650  gruina  10773  ltrnq  10934  ltsosr  11049  ltasr  11055  axpre-lttri  11120  axpre-ltadd  11122  nn0sub  12528  zextle  12643  zextlt  12644  xlesubadd  13263  sqeqor  14226  nn0opth2  14282  rexfiuz  15358  climshft  15586  rpnnen2lem10  16238  dvdsext  16338  ltoddhalfle  16378  halfleoddlt  16379  sumodd  16405  sadcadd  16475  dvdssq  16584  rpexp  16740  pcdvdsb  16888  imasleval  17554  isacs2  17668  acsfiel  17669  funcres2b  17913  pospropd  18340  isnsg  19179  nsgbi  19181  elnmz  19187  nmzbi  19188  oddvdsnn0  19567  odeq  19573  odmulg  19579  isslw  19631  slwispgp  19634  gsumval3lem2  19929  gsumcom2  19998  abveq0  20847  cnt0  23386  kqfvima  23770  kqt0lem  23776  isr0  23777  r0cld  23778  regr1lem2  23780  nrmr0reg  23789  isfildlem  23897  cnextfvval  24105  xmeteq0  24378  imasf1oxmet  24415  comet  24553  dscmet  24612  nrmmetd  24614  tngngp  24694  tngngp3  24696  mbfsup  25706  mbfinf  25707  degltlem1  26112  logltb  26642  cxple2  26739  rlimcnp  27007  rlimcnp2  27008  isppw2  27156  sqf11  27180  lesrec  27869  tgjustc1  28621  tgjustc2  28622  f1otrgitv  29016  nbuhgr2vtx1edgb  29499  dfconngr1  30336  eupth2lem3lem6  30381  nmlno0i  30943  nmlno0  30944  blocn  30956  ubth  31022  hvsubeq0  31217  hvaddcan  31219  hvsubadd  31226  normsub0  31285  hlim2  31341  pjoc1  31583  pjoc2  31588  chne0  31643  chsscon3  31649  chlejb1  31661  chnle  31663  h1de2ci  31705  elspansn  31715  elspansn2  31716  cmbr3  31757  cmcm  31763  cmcm3  31764  pjch1  31819  pjch  31843  pj11  31863  pjnel  31875  eigorth  31987  elnlfn  32077  nmlnop0  32147  lnopeq  32158  lnopcon  32184  lnfncon  32205  pjdifnormi  32316  chrelat2  32519  cvexch  32523  mdsym  32561  eqelbid  32622  fmptcof2  32809  mgcoval  33125  mgcval  33126  mgccole1  33129  mgccole2  33130  mgcmnt1  33131  mgcmnt2  33132  mgccnv  33138  domnprodeq0  33421  unitprodclb  33536  ist0cld  34091  zarclssn  34131  zart0  34137  signswch  34819  fnrelpredd  35351  r1omhfb  35372  r1omhfbregs  35397  axsepg2  35400  axsepg4  35403  cvmlift2lem12  35628  cvmlift2lem13  35629  satfv1lem  35676  satf0op  35691  fmlafvel  35699  abs2sqle  35994  abs2sqlt  35995  axextdist  36111  brimageg  36239  brdomaing  36247  brrangeg  36248  elhf2  36489  nn0prpwlem  36646  nn0prpw  36647  onsuct0  36765  ttcwf2  36849  bj-sbceqgALT  37351  bj-elabd2ALT  37374  eleq2w2ALT  37496  bj-axseprep  37523  dfgcd3  37780  cbveud  37830  wl-3xorbi123d  37933  wl-dfcleq  37972  matunitlindf  38081  prdsbnd2  38258  isdrngo1  38419  eqrelf  38721  elsymrels5  39103  dfdisjs5  39260  eldisjs5  39286  mpets2  39418  pets  39429  lsatcmp  39591  llnexchb2  40457  lautset  40670  lautle  40672  sticksstones2  42728  aks6d1c7  42765  dvdsexpnn0  42907  eu6w  43222  abbibw  43223  zindbi  43487  wepwsolem  43583  aomclem8  43602  onsupmaxb  43780  oaordnr  43837  omnord1  43846  oenord1  43857  ntrneik13  44638  ntrneix13  44639  ntrneik4w  44640  2sbc6g  44955  2sbc5g  44956  modelaxreplem3  45520  wessf1ornlem  45727  fourierdlem31  46676  fourierdlem42  46687  fourierdlem54  46698  funressndmafv2rn  47781  dfatbrafv2b  47803  fnbrafv2b  47806  ichbidv  48023  ichnfim  48034  sprsymrelf  48065  sprsymrelfo  48067  isuspgrimlem  48481  line2ylem  49337  line2xlem  49339  mofeu  49433  tposres0  49462  catprslem  49595