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 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bi2bian9  652  xorbi12d  1555  norass  1567  ru0  2166  sbbib  2393  sb8eulem  2626  abbibOLD  2833  cleqh  2893  cleqf  2954  vtoclbg  3523  vtoclb  3532  ceqsexg  3610  elabgf  3631  reu6  3687  sbcbig  3793  unineq  4236  sbcnestgfw  4382  sbcnestgf  4387  preq12bg  4811  axrep1  5237  nalsetOLD  5273  opthg  5451  opelopabsb  5509  isso2i  5601  opeliunxp2  5822  resieq  5993  dfpo2  6320  cbviotaw  6522  cbviota  6524  iota2df  6547  fnbrfvb  6961  fvelimab  6983  fvopab5  7053  fmptco  7157  fsng  7165  fressnfv  7191  fnpr2g  7242  isorel  7360  isocnv  7364  isocnv3  7366  isotr  7370  eqfunresadj  7396  ovg  7612  caovcang  7649  caovordg  7655  caovord3d  7658  caovord  7659  caofidlcan  7758  orduninsuc  7881  xpord2pred  8192  xpord3pred  8199  opeliunxp2f  8258  brtpos  8283  dftpos4  8293  omopth  8702  ecopovsym  8871  xpf1o  9189  nneneq  9252  ttrclselem2  9757  r1pwALT  9890  elhf2  9940  kardenOLD  9990  infxpenlem  10122  aceq0  10227  cflim2  10371  zfac  10568  ttukeylem1  10617  axextnd  10706  axrepndlem1  10707  axrepndlem2  10708  axrepnd  10709  axacndlem5  10726  zfcndrep  10729  zfcndac  10734  winalim  10810  gruina  10933  ltrnq  11094  ltsosr  11209  ltasr  11215  axpre-lttri  11280  axpre-ltadd  11282  nn0sub  12686  zextle  12802  zextlt  12803  xlesubadd  13423  sqeqor  14390  nn0opth2  14446  rexfiuz  15547  climshft  15775  rpnnen2lem10  16423  dvdsext  16523  ltoddhalfle  16563  halfleoddlt  16564  sumodd  16590  sadcadd  16660  dvdssq  16774  rpexp  16930  pcdvdsb  17079  imasleval  17745  isacs2  17859  acsfiel  17860  funcres2b  18104  pospropd  18531  isnsg  19397  nsgbi  19399  elnmz  19405  nmzbi  19406  oddvdsnn0  19791  odeq  19797  odmulg  19803  isslw  19855  slwispgp  19858  gsumval3lem2  20153  gsumcom2  20222  abveq0  21108  matunitlindf  23029  cnt0  23697  kqfvima  24082  kqt0lem  24088  isr0  24089  r0cld  24090  regr1lem2  24092  nrmr0reg  24101  isfildlem  24209  cnextfvval  24417  xmeteq0  24690  imasf1oxmet  24727  comet  24865  dscmet  24924  nrmmetd  24926  tngngp  25006  tngngp3  25008  mbfsup  26018  mbfinf  26019  degltlem1  26423  logltb  26961  cxple2  27058  rlimcnp  27326  rlimcnp2  27327  isppw2  27475  sqf11  27499  lesrec  28218  tgjustc1  28970  tgjustc2  28971  f1otrgitv  29480  nbuhgr2vtx1edgb  29966  dfconngr1  30822  eupth2lem3lem6  30867  nmlno0i  31429  nmlno0  31430  blocn  31442  ubth  31508  hvsubeq0  31703  hvaddcan  31705  hvsubadd  31712  normsub0  31771  hlim2  31827  pjoc1  32069  pjoc2  32074  chne0  32129  chsscon3  32135  chlejb1  32147  chnle  32149  h1de2ci  32191  elspansn  32201  elspansn2  32202  cmbr3  32243  cmcm  32249  cmcm3  32250  pjch1  32305  pjch  32329  pj11  32349  pjnel  32361  eigorth  32473  elnlfn  32563  nmlnop0  32633  lnopeq  32644  lnopcon  32670  lnfncon  32691  pjdifnormi  32802  chrelat2  33005  cvexch  33009  mdsym  33047  eqelbid  33146  fmptcof2  33326  mgcoval  33623  mgcval  33624  mgccole1  33627  mgccole2  33628  mgcmnt1  33629  mgcmnt2  33630  mgccnv  33636  domnprodeq0  33916  unitprodclb  34028  ist0cld  34548  zarclssn  34588  zart0  34594  signswch  35273  reu6f  35792  fnrelpredd  35817  eqhf  35833  eqhfregs  35918  axsepg2  35921  axsepg4  35924  cvmlift2lem12  36259  cvmlift2lem13  36260  satfv1lem  36307  satf0op  36322  fmlafvel  36330  abs2sqle  36625  abs2sqlt  36626  axextdist  36752  brimageg  36880  brdomaing  36888  brrangeg  36889  nn0prpwlem  37301  nn0prpw  37302  onsuct0  37420  ttcwf2  37504  bj-sbceqgALT  38005  bj-elabd2ALT  38029  eleq2w2ALT  38166  bj-axseprep  38194  dfgcd3  38450  cbveud  38500  wl-3xorbi123d  38603  wl-dfcleq  38642  prdsbnd2  38932  isdrngo1  39093  eqrelf  39393  elsymrels5  39775  dfdisjs5  39932  eldisjs5  39958  mpets2  40090  pets  40101  lsatcmp  40263  llnexchb2  41129  lautset  41342  lautle  41344  sticksstones2  43400  aks6d1c7  43437  dvdsexpnn0  43590  eu6w  43891  abbibw  43892  zindbi  44157  wepwsolem  44253  aomclem8  44267  onsupmaxb  44444  oaordnr  44501  omnord1  44510  oenord1  44521  ntrneik13  45301  ntrneix13  45302  ntrneik4w  45303  2sbc6g  45602  2sbc5g  45603  modelaxreplem3  46176  wessf1ornlem  46415  fourierdlem31  47363  fourierdlem42  47374  fourierdlem54  47385  funressndmafv2rn  48508  dfatbrafv2b  48530  fnbrafv2b  48533  ichbidv  48750  ichnfim  48761  sprsymrelf  48792  sprsymrelfo  48794  isuspgrimlem  49208  line2ylem  50078  line2xlem  50080  mofeu  50174  tposres0  50205  catprslem  50339