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  4381  fnprb  7185  fntpb  7186  eqfunresadj  7338  eloprabga  7501  ordsucuniel  7802  ordsucun  7803  oeoa  8564  ereldm  8727  boxcutc  8917  mapen  9111  mapfien  9366  wemapwe  9657  sdom2en01  10262  prlem936  11007  subcan  11484  mulcan1g  11838  conjmul  11906  ltrec  12072  rebtwnz  12913  xposdif  13229  divelunit  13462  fseq1m1p1  13567  fzm1  13575  fllt  13775  hashfacen  14426  hashf1  14429  ccat0  14548  lenegsq  15294  dvdsmod  16306  bitsmod  16413  smueqlem  16467  rpexp  16699  eulerthlem2  16759  odzdvds  16773  pcelnn  16848  xpsle  17549  isepi  17709  fthmon  17898  cat1  18066  pospropd  18293  grpidpropd  18596  mgmhmpropd  18632  sgrppropd  18665  mndpropd  18693  mhmpropd  18726  grppropd  18890  ghmnsgima  19179  mndodcong  19479  odf1  19499  odf1o1  19509  sylow3lem6  19569  lsmcntzr  19617  efgredlema  19677  cmnpropd  19728  qusecsub  19772  dprdf11  19962  rngpropd  20090  ringpropd  20204  dvdsrpropd  20332  resrhm2b  20518  abvpropd  20751  lmodprop2d  20837  lsspropd  20931  lmhmpropd  20987  lbspropd  21013  lvecvscan  21028  lvecvscan2  21029  chrnzr  21447  zndvds0  21467  ip2eq  21569  phlpropd  21571  assapropd  21788  qtopcn  23608  tsmsf1o  24039  xmetgt0  24253  txmetcnp  24442  metustsym  24450  nlmmul0or  24578  cnmet  24666  evth  24865  isclmp  25004  minveclem3b  25335  mbfposr  25560  itg2cn  25671  iblcnlem  25697  dvcvx  25932  ulm2  26301  efeq1  26444  dcubic  26763  mcubic  26764  dquart  26770  birthdaylem3  26870  ftalem2  26991  issqf  27053  sqff1o  27099  bposlem7  27208  lgsabs1  27254  gausslemma2dlem1a  27283  lgsquadlem2  27299  addsq2reu  27358  dchrisum0lem1  27434  sltrec  27739  opphllem6  28686  colhp  28704  lmiinv  28726  lmiopp  28736  wlkeq  29569  eupth2lem3lem3  30166  eupth2lem3lem6  30169  nmounbi  30712  ip2eqi  30792  hvmulcan  31008  hvsubcan2  31011  hi2eq  31041  fh2  31555  riesz4i  31999  cvbr4i  32303  sgnmulsgn  32774  sgnmulsgp  32775  xdivpnfrp  32860  isorng  33284  qusker  33327  ellspds  33346  ply1moneq  33562  ballotlemfc0  34491  ballotlemfcc  34492  subfacp1lem5  35178  topfneec2  36351  neibastop3  36357  unccur  37604  cos2h  37612  tan2h  37613  poimirlem25  37646  poimirlem27  37648  dvasin  37705  caures  37761  ismtyima  37804  isdmn3  38075  dmecd  38299  releldmqscoss  38659  tendospcanN  41024  dochsncom  41383  f1o2d2  42228  sqrtcval  43637  or3or  44019  neicvgel1  44115  rusbcALT  44435  sbcoreleleqVD  44855  climreeq  45618  coseq0  45869  modmkpkne  47366  affinecomb1  48695  eenglngeehlnmlem1  48730  2sphere  48742  line2  48745  itscnhlc0yqe  48752  itscnhlc0xyqsol  48758  oduoppcciso  49559