Theorem 3bitr3d 309

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbcne12  4356  fnprb  7163  fntpb  7164  eqfunresadj  7315  eloprabga  7476  ordsucuniel  7775  ordsucun  7776  oeoa  8533  ereldm  8697  boxcutc  8889  mapen  9079  mapfien  9321  wemapwe  9618  sdom2en01  10224  prlem936  10970  subcan  11449  mulcan1g  11803  conjmul  11872  ltrec  12038  rebtwnz  12897  xposdif  13214  divelunit  13447  fseq1m1p1  13553  fzm1  13561  fllt  13765  hashfacen  14416  hashf1  14419  ccat0  14538  lenegsq  15283  dvdsmod  16298  bitsmod  16405  smueqlem  16459  rpexp  16692  eulerthlem2  16752  odzdvds  16766  pcelnn  16841  xpsle  17543  isepi  17707  fthmon  17896  cat1  18064  pospropd  18291  grpidpropd  18630  mgmhmpropd  18666  sgrppropd  18699  mndpropd  18727  mhmpropd  18760  grppropd  18927  ghmnsgima  19215  mndodcong  19517  odf1  19537  odf1o1  19547  sylow3lem6  19607  lsmcntzr  19655  efgredlema  19715  cmnpropd  19766  qusecsub  19810  dprdf11  20000  rngpropd  20155  ringpropd  20269  dvdsrpropd  20396  resrhm2b  20579  abvpropd  20812  isorng  20838  lmodprop2d  20919  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  lvecvscan  21109  lvecvscan2  21110  chrnzr  21510  zndvds0  21530  ip2eq  21633  phlpropd  21635  assapropd  21851  qtopcn  23679  tsmsf1o  24110  xmetgt0  24323  txmetcnp  24512  metustsym  24520  nlmmul0or  24648  cnmet  24736  evth  24926  isclmp  25064  minveclem3b  25395  mbfposr  25619  itg2cn  25730  iblcnlem  25756  dvcvx  25987  ulm2  26350  efeq1  26492  dcubic  26810  mcubic  26811  dquart  26817  birthdaylem3  26917  ftalem2  27037  issqf  27099  sqff1o  27145  bposlem7  27253  lgsabs1  27299  gausslemma2dlem1a  27328  lgsquadlem2  27344  addsq2reu  27403  dchrisum0lem1  27479  sltssnb  27761  ltsrec  27793  opphllem6  28820  colhp  28838  lmiinv  28860  lmiopp  28870  wlkeq  29702  eupth2lem3lem3  30300  eupth2lem3lem6  30303  nmounbi  30847  ip2eqi  30927  hvmulcan  31143  hvsubcan2  31146  hi2eq  31176  fh2  31690  riesz4i  32134  cvbr4i  32438  sgnmulsgn  32915  sgnmulsgp  32916  xdivpnfrp  32992  qusker  33409  ellspds  33428  ply1moneq  33648  ballotlemfc0  34637  ballotlemfcc  34638  subfacp1lem5  35366  topfneec2  36538  neibastop3  36544  unccur  37924  cos2h  37932  tan2h  37933  poimirlem25  37966  poimirlem27  37968  dvasin  38025  caures  38081  ismtyima  38124  isdmn3  38395  dmecd  38631  releldmqscoss  39066  tendospcanN  41469  dochsncom  41828  f1o2d2  42674  sqrtcval  44068  or3or  44450  neicvgel1  44546  rusbcALT  44865  sbcoreleleqVD  45285  climreeq  46043  coseq0  46292  modmkpkne  47809  affinecomb1  49172  eenglngeehlnmlem1  49207  2sphere  49219  line2  49222  itscnhlc0yqe  49229  itscnhlc0xyqsol  49235  oduoppcciso  50035