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  2164  sbbib  2391  sb8eulem  2624  abbib  2830  cleqh  2890  cleqf  2951  vtoclbg  3520  vtoclb  3529  ceqsexg  3607  elabgf  3628  reu6  3684  sbcbig  3790  unineq  4234  sbcnestgfw  4379  sbcnestgf  4384  preq12bg  4813  axrep1  5233  nalsetOLD  5269  opthg  5446  opelopabsb  5504  isso2i  5596  opeliunxp2  5815  resieq  5981  dfpo2  6292  cbviotaw  6494  cbviota  6496  iota2df  6518  fnbrfvb  6927  fvelimab  6949  fvopab5  7019  fmptco  7122  fsng  7130  fressnfv  7156  fnpr2g  7208  isorel  7326  isocnv  7330  isocnv3  7332  isotr  7336  eqfunresadj  7362  ovg  7577  caovcang  7614  caovordg  7620  caovord3d  7623  caovord  7624  caofidlcan  7720  orduninsuc  7843  xpord2pred  8146  xpord3pred  8153  opeliunxp2f  8211  brtpos  8236  dftpos4  8246  omopth  8655  ecopovsym  8824  xpf1o  9142  nneneq  9205  ttrclselem2  9711  r1pwALT  9841  elhf2  9891  kardenOLD  9941  infxpenlem  10073  aceq0  10178  cflim2  10322  zfac  10519  ttukeylem1  10568  axextnd  10657  axrepndlem1  10658  axrepndlem2  10659  axrepnd  10660  axacndlem5  10677  zfcndrep  10680  zfcndac  10685  winalim  10761  gruina  10884  ltrnq  11045  ltsosr  11160  ltasr  11166  axpre-lttri  11231  axpre-ltadd  11233  nn0sub  12637  zextle  12753  zextlt  12754  xlesubadd  13374  sqeqor  14340  nn0opth2  14396  rexfiuz  15495  climshft  15723  rpnnen2lem10  16371  dvdsext  16471  ltoddhalfle  16511  halfleoddlt  16512  sumodd  16538  sadcadd  16608  dvdssq  16722  rpexp  16878  pcdvdsb  17027  imasleval  17693  isacs2  17807  acsfiel  17808  funcres2b  18052  pospropd  18479  isnsg  19345  nsgbi  19347  elnmz  19353  nmzbi  19354  oddvdsnn0  19738  odeq  19744  odmulg  19750  isslw  19802  slwispgp  19805  gsumval3lem2  20100  gsumcom2  20169  abveq0  21055  matunitlindf  22976  cnt0  23644  kqfvima  24029  kqt0lem  24035  isr0  24036  r0cld  24037  regr1lem2  24039  nrmr0reg  24048  isfildlem  24156  cnextfvval  24364  xmeteq0  24637  imasf1oxmet  24674  comet  24812  dscmet  24871  nrmmetd  24873  tngngp  24953  tngngp3  24955  mbfsup  25965  mbfinf  25966  degltlem1  26370  logltb  26910  cxple2  27007  rlimcnp  27275  rlimcnp2  27276  isppw2  27424  sqf11  27448  lesrec  28167  tgjustc1  28919  tgjustc2  28920  f1otrgitv  29429  nbuhgr2vtx1edgb  29915  dfconngr1  30771  eupth2lem3lem6  30816  nmlno0i  31378  nmlno0  31379  blocn  31391  ubth  31457  hvsubeq0  31652  hvaddcan  31654  hvsubadd  31661  normsub0  31720  hlim2  31776  pjoc1  32018  pjoc2  32023  chne0  32078  chsscon3  32084  chlejb1  32096  chnle  32098  h1de2ci  32140  elspansn  32150  elspansn2  32151  cmbr3  32192  cmcm  32198  cmcm3  32199  pjch1  32254  pjch  32278  pj11  32298  pjnel  32310  eigorth  32422  elnlfn  32512  nmlnop0  32582  lnopeq  32593  lnopcon  32619  lnfncon  32640  pjdifnormi  32751  chrelat2  32954  cvexch  32958  mdsym  32996  eqelbid  33053  fmptcof2  33233  mgcoval  33529  mgcval  33530  mgccole1  33533  mgccole2  33534  mgcmnt1  33535  mgcmnt2  33536  mgccnv  33542  domnprodeq0  33822  unitprodclb  33926  ist0cld  34447  zarclssn  34487  zart0  34493  signswch  35173  fnrelpredd  35699  r1omhfb  35717  r1omhfbregs  35778  axsepg2  35781  axsepg4  35784  cvmlift2lem12  36048  cvmlift2lem13  36049  satfv1lem  36096  satf0op  36111  fmlafvel  36119  abs2sqle  36414  abs2sqlt  36415  axextdist  36531  brimageg  36659  brdomaing  36667  brrangeg  36668  nn0prpwlem  37080  nn0prpw  37081  onsuct0  37199  ttcwf2  37283  bj-sbceqgALT  37784  bj-elabd2ALT  37808  eleq2w2ALT  37930  bj-axseprep  37958  dfgcd3  38213  cbveud  38263  wl-3xorbi123d  38366  wl-dfcleq  38405  prdsbnd2  38697  isdrngo1  38858  eqrelf  39158  elsymrels5  39540  dfdisjs5  39697  eldisjs5  39723  mpets2  39855  pets  39866  lsatcmp  40028  llnexchb2  40894  lautset  41107  lautle  41109  sticksstones2  43165  aks6d1c7  43202  dvdsexpnn0  43354  eu6w  43641  abbibw  43642  zindbi  43906  wepwsolem  44002  aomclem8  44021  onsupmaxb  44199  oaordnr  44256  omnord1  44265  oenord1  44276  ntrneik13  45057  ntrneix13  45058  ntrneik4w  45059  2sbc6g  45358  2sbc5g  45359  modelaxreplem3  45922  wessf1ornlem  46143  fourierdlem31  47092  fourierdlem42  47103  fourierdlem54  47114  funressndmafv2rn  48237  dfatbrafv2b  48259  fnbrafv2b  48262  ichbidv  48479  ichnfim  48490  sprsymrelf  48521  sprsymrelfo  48523  isuspgrimlem  48937  line2ylem  49807  line2xlem  49809  mofeu  49902  tposres0  49929  catprslem  50062