Theorem bibi12d 335

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  bi2bian9  918  xorbi12d  1475  sb8eu  2502  cleqh  2721  vtoclb  3253  vtoclbg  3257  ceqsexg  3322  elabgf  3336  reu6  3382  ru  3421  sbcbig  3467  unineq  3859  sbcnestgf  3973  preq12bg  4361  prel12g  4362  axrep1  4742  axrep4  4745  nalset  4765  opthg  4916  opelopabsb  4955  isso2i  5037  opeliunxp2  5230  resieq  5376  elimasng  5460  cbviota  5825  iota2df  5844  fnbrfvb  6203  fvelimab  6220  fvopab5  6275  fmptco  6362  fsng  6369  fsn2g  6370  fressnfv  6392  fnpr2g  6439  isorel  6541  isocnv  6545  isocnv3  6547  isotr  6551  ovg  6764  caovcang  6800  caovordg  6806  caovord3d  6809  caovord  6810  orduninsuc  7005  opeliunxp2f  7296  brtpos  7321  dftpos4  7331  omopth  7698  ecopovsym  7809  xpf1o  8082  nneneq  8103  r1pwALT  8669  karden  8718  infxpenlem  8796  aceq0  8901  cflim2  9045  zfac  9242  ttukeylem1  9291  axextnd  9373  axrepndlem1  9374  axrepndlem2  9375  axrepnd  9376  axacndlem5  9393  zfcndrep  9396  zfcndac  9401  winalim  9477  gruina  9600  ltrnq  9761  ltsosr  9875  ltasr  9881  axpre-lttri  9946  axpre-ltadd  9948  nn0sub  11303  zextle  11410  zextlt  11411  xlesubadd  12052  sqeqor  12934  nn0opth2  13015  rexfiuz  14037  climshft  14257  rpnnen2lem10  14896  dvdsext  14986  ltoddhalfle  15028  halfleoddlt  15029  sumodd  15054  sadcadd  15123  dvdssq  15223  isprm2lem  15337  rpexp  15375  pcdvdsb  15516  imasleval  16141  isacs2  16254  acsfiel  16255  funcres2b  16497  pospropd  17074  isnsg  17563  nsgbi  17565  elnmz  17573  nmzbi  17574  oddvdsnn0  17903  odeq  17909  odmulg  17913  isslw  17963  slwispgp  17966  gsumval3lem2  18247  gsumcom2  18314  abveq0  18766  cnt0  21090  kqfvima  21473  kqt0lem  21479  isr0  21480  r0cld  21481  regr1lem2  21483  nrmr0reg  21492  isfildlem  21601  cnextfvval  21809  xmeteq0  22083  imasf1oxmet  22120  comet  22258  dscmet  22317  nrmmetd  22319  tngngp  22398  tngngp3  22400  mbfsup  23371  mbfinf  23372  degltlem1  23770  logltb  24284  cxple2  24377  rlimcnp  24626  rlimcnp2  24627  isppw2  24775  sqf11  24799  f1otrgitv  25684  nbuhgr2vtx1edgb  26169  dfconngr1  26948  eupth2lem3lem6  26993  nmlno0i  27537  nmlno0  27538  blocn  27550  ubth  27617  hvsubeq0  27813  hvaddcan  27815  hvsubadd  27822  normsub0  27881  hlim2  27937  pjoc1  28181  pjoc2  28186  chne0  28241  chsscon3  28247  chlejb1  28259  chnle  28261  h1de2ci  28303  elspansn  28313  elspansn2  28314  cmbr3  28355  cmcm  28361  cmcm3  28362  pjch1  28417  pjch  28441  pj11  28461  pjnel  28473  eigorth  28585  elnlfn  28675  nmlnop0  28745  lnopeq  28756  lnopcon  28782  lnfncon  28803  pjdifnormi  28914  chrelat2  29117  cvexch  29121  mdsym  29159  fmptcof2  29340  signswch  30460  cvmlift2lem12  31057  cvmlift2lem13  31058  abs2sqle  31335  abs2sqlt  31336  dfpo2  31406  br1steqg  31429  br2ndeqg  31430  axextdist  31459  brimageg  31729  brdomaing  31737  brrangeg  31738  elhf2  31977  nn0prpwlem  32012  nn0prpw  32013  onsuct0  32135  bj-abbi  32471  bj-axrep1  32484  bj-axrep4  32487  bj-nalset  32490  bj-sbceqgALT  32597  bj-ru0  32632  matunitlindf  33078  prdsbnd2  33265  isdrngo1  33426  lsatcmp  33809  llnexchb2  34674  lautset  34887  lautle  34889  zindbi  37030  wepwsolem  37131  aomclem8  37150  ntrneik13  37917  ntrneix13  37918  ntrneik4w  37919  2sbc6g  38137  2sbc5g  38138  wessf1ornlem  38880  fourierdlem31  39692  fourierdlem42  39703  fourierdlem54  39714  sprsymrelf  41063  sprsymrelfo  41065