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  6300  cbviotaw  6502  cbviota  6504  iota2df  6526  fnbrfvb  6936  fvelimab  6958  fvopab5  7028  fmptco  7131  fsng  7139  fressnfv  7165  fnpr2g  7217  isorel  7335  isocnv  7339  isocnv3  7341  isotr  7345  eqfunresadj  7371  ovg  7586  caovcang  7623  caovordg  7629  caovord3d  7632  caovord  7633  caofidlcan  7732  orduninsuc  7855  xpord2pred  8163  xpord3pred  8170  opeliunxp2f  8228  brtpos  8253  dftpos4  8263  omopth  8672  ecopovsym  8841  xpf1o  9159  nneneq  9222  ttrclselem2  9728  r1pwALT  9861  elhf2  9911  kardenOLD  9961  infxpenlem  10093  aceq0  10198  cflim2  10342  zfac  10539  ttukeylem1  10588  axextnd  10677  axrepndlem1  10678  axrepndlem2  10679  axrepnd  10680  axacndlem5  10697  zfcndrep  10700  zfcndac  10705  winalim  10781  gruina  10904  ltrnq  11065  ltsosr  11180  ltasr  11186  axpre-lttri  11251  axpre-ltadd  11253  nn0sub  12657  zextle  12773  zextlt  12774  xlesubadd  13394  sqeqor  14361  nn0opth2  14417  rexfiuz  15516  climshft  15744  rpnnen2lem10  16392  dvdsext  16492  ltoddhalfle  16532  halfleoddlt  16533  sumodd  16559  sadcadd  16629  dvdssq  16743  rpexp  16899  pcdvdsb  17048  imasleval  17714  isacs2  17828  acsfiel  17829  funcres2b  18073  pospropd  18500  isnsg  19366  nsgbi  19368  elnmz  19374  nmzbi  19375  oddvdsnn0  19759  odeq  19765  odmulg  19771  isslw  19823  slwispgp  19826  gsumval3lem2  20121  gsumcom2  20190  abveq0  21076  matunitlindf  22997  cnt0  23665  kqfvima  24050  kqt0lem  24056  isr0  24057  r0cld  24058  regr1lem2  24060  nrmr0reg  24069  isfildlem  24177  cnextfvval  24385  xmeteq0  24658  imasf1oxmet  24695  comet  24833  dscmet  24892  nrmmetd  24894  tngngp  24974  tngngp3  24976  mbfsup  25986  mbfinf  25987  degltlem1  26391  logltb  26929  cxple2  27026  rlimcnp  27294  rlimcnp2  27295  isppw2  27443  sqf11  27467  lesrec  28186  tgjustc1  28938  tgjustc2  28939  f1otrgitv  29448  nbuhgr2vtx1edgb  29934  dfconngr1  30790  eupth2lem3lem6  30835  nmlno0i  31397  nmlno0  31398  blocn  31410  ubth  31476  hvsubeq0  31671  hvaddcan  31673  hvsubadd  31680  normsub0  31739  hlim2  31795  pjoc1  32037  pjoc2  32042  chne0  32097  chsscon3  32103  chlejb1  32115  chnle  32117  h1de2ci  32159  elspansn  32169  elspansn2  32170  cmbr3  32211  cmcm  32217  cmcm3  32218  pjch1  32273  pjch  32297  pj11  32317  pjnel  32329  eigorth  32441  elnlfn  32531  nmlnop0  32601  lnopeq  32612  lnopcon  32638  lnfncon  32659  pjdifnormi  32770  chrelat2  32973  cvexch  32977  mdsym  33015  eqelbid  33072  fmptcof2  33252  mgcoval  33548  mgcval  33549  mgccole1  33552  mgccole2  33553  mgcmnt1  33554  mgcmnt2  33555  mgccnv  33561  domnprodeq0  33841  unitprodclb  33945  ist0cld  34466  zarclssn  34506  zart0  34512  signswch  35191  fnrelpredd  35721  r1omhfb  35739  r1omhfbregs  35806  axsepg2  35809  axsepg4  35812  cvmlift2lem12  36080  cvmlift2lem13  36081  satfv1lem  36128  satf0op  36143  fmlafvel  36151  abs2sqle  36446  abs2sqlt  36447  axextdist  36562  brimageg  36690  brdomaing  36698  brrangeg  36699  nn0prpwlem  37111  nn0prpw  37112  onsuct0  37230  ttcwf2  37314  bj-sbceqgALT  37815  bj-elabd2ALT  37839  eleq2w2ALT  37963  bj-axseprep  37991  dfgcd3  38247  cbveud  38297  wl-3xorbi123d  38400  wl-dfcleq  38439  prdsbnd2  38731  isdrngo1  38892  eqrelf  39192  elsymrels5  39574  dfdisjs5  39731  eldisjs5  39757  mpets2  39889  pets  39900  lsatcmp  40062  llnexchb2  40928  lautset  41141  lautle  41143  sticksstones2  43199  aks6d1c7  43236  dvdsexpnn0  43388  eu6w  43689  abbibw  43690  zindbi  43954  wepwsolem  44050  aomclem8  44064  onsupmaxb  44242  oaordnr  44299  omnord1  44308  oenord1  44319  ntrneik13  45099  ntrneix13  45100  ntrneik4w  45101  2sbc6g  45400  2sbc5g  45401  modelaxreplem3  45971  wessf1ornlem  46201  fourierdlem31  47149  fourierdlem42  47160  fourierdlem54  47171  funressndmafv2rn  48294  dfatbrafv2b  48316  fnbrafv2b  48319  ichbidv  48536  ichnfim  48547  sprsymrelf  48578  sprsymrelfo  48580  isuspgrimlem  48994  line2ylem  49864  line2xlem  49866  mofeu  49959  tposres0  49986  catprslem  50119