Theorem 3bitr3d 308

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbcne12  4351  fnprb  7078  fntpb  7079  eloprabga  7373  eloprabgaOLD  7374  ordsucuniel  7659  ordsucun  7660  oeoa  8404  ereldm  8520  boxcutc  8703  mapen  8893  mapfien  9128  wemapwe  9416  sdom2en01  10042  prlem936  10787  subcan  11259  mulcan1g  11611  conjmul  11675  ltrec  11840  rebtwnz  12669  xposdif  12978  divelunit  13208  fseq1m1p1  13313  fzm1  13318  fllt  13507  hashfacen  14147  hashfacenOLD  14148  hashf1  14152  ccat0  14261  lenegsq  15013  dvdsmod  16019  bitsmod  16124  smueqlem  16178  rpexp  16408  eulerthlem2  16464  odzdvds  16477  pcelnn  16552  xpsle  17271  isepi  17433  fthmon  17624  cat1  17793  pospropd  18026  grpidpropd  18327  mndpropd  18391  mhmpropd  18417  grppropd  18575  ghmnsgima  18839  mndodcong  19131  odf1  19150  odf1o1  19158  sylow3lem6  19218  lsmcntzr  19267  efgredlema  19327  cmnpropd  19377  dprdf11  19607  ringpropd  19802  dvdsrpropd  19919  abvpropd  20083  lmodprop2d  20166  lsspropd  20260  lmhmpropd  20316  lbspropd  20342  lvecvscan  20354  lvecvscan2  20355  chrnzr  20715  zndvds0  20739  ip2eq  20839  phlpropd  20841  assapropd  21057  qtopcn  22846  tsmsf1o  23277  xmetgt0  23492  txmetcnp  23684  metustsym  23692  nlmmul0or  23828  cnmet  23916  evth  24103  isclmp  24241  minveclem3b  24573  mbfposr  24797  itg2cn  24909  iblcnlem  24934  dvcvx  25165  ulm2  25525  efeq1  25665  dcubic  25977  mcubic  25978  dquart  25984  birthdaylem3  26084  ftalem2  26204  issqf  26266  sqff1o  26312  bposlem7  26419  lgsabs1  26465  gausslemma2dlem1a  26494  lgsquadlem2  26510  addsq2reu  26569  dchrisum0lem1  26645  opphllem6  27094  colhp  27112  lmiinv  27134  lmiopp  27144  wlkeq  27981  eupth2lem3lem3  28573  eupth2lem3lem6  28576  nmounbi  29117  ip2eqi  29197  hvmulcan  29413  hvsubcan2  29416  hi2eq  29446  fh2  29960  riesz4i  30404  cvbr4i  30708  xdivpnfrp  31186  isorng  31477  qusker  31528  ellspds  31543  ballotlemfc0  32438  ballotlemfcc  32439  sgnmulsgn  32495  sgnmulsgp  32496  subfacp1lem5  33125  eqfunresadj  33714  sltrec  33993  topfneec2  34524  neibastop3  34530  unccur  35739  cos2h  35747  tan2h  35748  poimirlem25  35781  poimirlem27  35783  dvasin  35840  caures  35897  ismtyima  35940  isdmn3  36211  dmecd  36419  releldmqscoss  36751  tendospcanN  39016  dochsncom  39375  sqrtcval  41202  or3or  41584  neicvgel1  41682  rusbcALT  42010  sbcoreleleqVD  42432  climreeq  43108  coseq0  43359  mgmhmpropd  45291  affinecomb1  46000  eenglngeehlnmlem1  46035  2sphere  46047  line2  46050  itscnhlc0yqe  46057  itscnhlc0xyqsol  46063