Theorem 3bitr3d 310

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 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 280	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sbcne12  4350  fnprb  7159  fntpb  7160  eqfunresadj  7311  eloprabga  7472  ordsucuniel  7771  ordsucun  7772  mpof1o2d  8072  oeoa  8530  ereldm  8694  boxcutc  8886  mapen  9076  mapfien  9318  wemapwe  9616  sdom2en01  10222  prlem936  10968  subcan  11447  mulcan1g  11801  conjmul  11870  ltrec  12036  rebtwnz  12895  xposdif  13212  divelunit  13445  fseq1m1p1  13551  fzm1  13559  fllt  13763  hashfacen  14414  hashf1  14417  ccat0  14536  lenegsq  15281  dvdsmod  16296  bitsmod  16403  smueqlem  16457  rpexp  16690  eulerthlem2  16750  odzdvds  16764  pcelnn  16839  xpsle  17541  isepi  17705  fthmon  17894  cat1  18062  pospropd  18289  grpidpropd  18628  mgmhmpropd  18664  sgrppropd  18697  mndpropd  18725  mhmpropd  18758  grppropd  18925  ghmnsgima  19213  mndodcong  19515  odf1  19535  odf1o1  19545  sylow3lem6  19605  lsmcntzr  19653  efgredlema  19713  cmnpropd  19764  qusecsub  19808  dprdf11  19998  rngpropd  20153  ringpropd  20267  dvdsrpropd  20394  resrhm2b  20581  abvpropd  20814  isorng  20840  lmodprop2d  20921  lsspropd  21014  lmhmpropd  21070  lbspropd  21096  lvecvscan  21111  lvecvscan2  21112  chrnzr  21512  zndvds0  21532  ip2eq  21635  phlpropd  21637  assapropd  21853  qtopcn  23704  tsmsf1o  24135  xmetgt0  24348  txmetcnp  24537  metustsym  24545  nlmmul0or  24673  cnmet  24761  evth  24951  isclmp  25089  minveclem3b  25420  mbfposr  25644  itg2cn  25755  iblcnlem  25781  dvcvx  26012  ulm2  26375  efeq1  26517  dcubic  26835  mcubic  26836  dquart  26842  birthdaylem3  26942  ftalem2  27062  issqf  27124  sqff1o  27170  bposlem7  27278  lgsabs1  27324  gausslemma2dlem1a  27353  lgsquadlem2  27369  addsq2reu  27428  dchrisum0lem1  27504  sltssnb  27786  ltsrec  27818  opphllem6  28845  colhp  28863  lmiinv  28885  lmiopp  28895  wlkeq  29727  eupth2lem3lem3  30325  eupth2lem3lem6  30328  nmounbi  30872  ip2eqi  30952  hvmulcan  31168  hvsubcan2  31171  hi2eq  31201  fh2  31715  riesz4i  32159  cvbr4i  32463  sgnmulsgn  32941  sgnmulsgp  32942  xdivpnfrp  33018  qusker  33439  ellspds  33458  ply1moneq  33678  ballotlemfc0  34684  ballotlemfcc  34685  subfacp1lem5  35413  topfneec2  36585  neibastop3  36591  unccur  37971  cos2h  37979  tan2h  37980  poimirlem25  38013  poimirlem27  38015  dvasin  38072  caures  38128  ismtyima  38171  isdmn3  38442  dmecd  38678  releldmqscoss  39113  tendospcanN  41516  dochsncom  41875  sqrtcval  44086  or3or  44468  neicvgel1  44564  rusbcALT  44883  sbcoreleleqVD  45303  climreeq  46059  coseq0  46308  modmkpkne  47831  affinecomb1  49194  eenglngeehlnmlem1  49229  2sphere  49241  line2  49244  itscnhlc0yqe  49251  itscnhlc0xyqsol  49257  oduoppcciso  50057