Theorem 3bitr3d 311

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

Ref	Expression
3bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))
3bitr3d.3	⊢ (𝜑 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
3bitr3d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr3d 283	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 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:  sbcne12  4368  fnprb  7186  fntpb  7187  eqfunresadj  7338  eloprabga  7499  ordsucuniel  7798  ordsucun  7799  mpof1o2d  8098  oeoa  8560  ereldm  8725  boxcutc  8917  mapen  9107  mapfien  9349  wemapwe  9647  sdom2en01  10254  prlem936  11000  subcan  11481  mulcan1g  11835  conjmul  11903  ltrec  12069  rebtwnz  12943  xposdif  13260  divelunit  13493  fseq1m1p1  13599  fzm1  13607  fllt  13811  hashfacen  14462  hashf1  14465  ccat0  14584  lenegsq  15329  dvdsmod  16344  bitsmod  16451  smueqlem  16505  rpexp  16738  eulerthlem2  16798  odzdvds  16812  pcelnn  16887  xpsle  17590  isepi  17754  fthmon  17943  cat1  18111  pospropd  18338  grpidpropd  18677  mgmhmpropd  18713  sgrppropd  18746  mndpropd  18774  mhmpropd  18807  grppropd  18974  ghmnsgima  19261  mndodcong  19563  odf1  19583  odf1o1  19593  sylow3lem6  19653  lsmcntzr  19701  efgredlema  19761  cmnpropd  19812  qusecsub  19856  dprdf11  20046  rngpropd  20201  ringpropd  20315  dvdsrpropd  20442  resrhm2b  20629  abvpropd  20862  isorng  20888  lmodprop2d  20969  lsspropd  21062  lmhmpropd  21118  lbspropd  21144  lvecvscan  21159  lvecvscan2  21160  chrnzr  21560  zndvds0  21580  ip2eq  21683  phlpropd  21685  assapropd  21901  qtopcn  23752  tsmsf1o  24183  xmetgt0  24396  txmetcnp  24585  metustsym  24593  nlmmul0or  24721  cnmet  24809  evth  24999  isclmp  25137  minveclem3b  25468  mbfposr  25692  itg2cn  25803  iblcnlem  25829  dvcvx  26060  ulm2  26423  efeq1  26568  dcubic  26886  mcubic  26887  dquart  26893  birthdaylem3  26993  ftalem2  27113  issqf  27175  sqff1o  27221  bposlem7  27329  lgsabs1  27375  gausslemma2dlem1a  27404  lgsquadlem2  27420  addsq2reu  27479  dchrisum0lem1  27555  sltssnb  27837  ltsrec  27869  opphllem6  28896  colhp  28914  lmiinv  28936  lmiopp  28946  wlkeq  29778  eupth2lem3lem3  30376  eupth2lem3lem6  30379  nmounbi  30923  ip2eqi  31003  hvmulcan  31219  hvsubcan2  31222  hi2eq  31252  fh2  31766  riesz4i  32210  cvbr4i  32514  sgnmulsgn  32992  sgnmulsgp  32993  xdivpnfrp  33069  qusker  33494  ellspds  33513  ply1moneq  33743  ballotlemfc0  34749  ballotlemfcc  34750  subfacp1lem5  35487  topfneec2  36669  neibastop3  36675  unccur  38055  cos2h  38063  tan2h  38064  poimirlem25  38097  poimirlem27  38099  dvasin  38156  caures  38212  ismtyima  38255  isdmn3  38526  dmecd  38762  releldmqscoss  39197  tendospcanN  41600  dochsncom  41959  sqrtcval  44170  or3or  44552  neicvgel1  44648  rusbcALT  44967  sbcoreleleqVD  45387  climreeq  46142  coseq0  46391  modmkpkne  47914  affinecomb1  49277  eenglngeehlnmlem1  49312  2sphere  49324  line2  49327  itscnhlc0yqe  49334  itscnhlc0xyqsol  49340  oduoppcciso  50140