Theorem 3bitr3d 276

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 248	. 2
4		3bitr3d.3	. 2
5	3, 4	bitrd 246	1

Syntax hints:  ->wi 4  <->wb 178

This theorem is referenced by:  sbcne12  3714  sbcne12gOLD  3715  csbcomgOLD  3725  fnprb  5951  eloprabga  6189  ordsucuniel  6445  ordsucun  6446  oeoa  7002  ereldm  7110  boxcutc  7269  mapen  7436  mapfien  7820  wemapwe  7821  sdom2en01  8353  prlem936  9095  subcan  9539  conjmul  9919  ltrec  10079  rebtwnz  10816  xposdif  11089  infmxrgelb  11161  fseq1m1p1  11387  fllt  11505  hashfacen  12054  hashf1  12057  lenegsq  12655  dvdsmod  13437  bitsmod  13479  smueqlem  13533  rpexp  13653  eulerthlem2  13704  odzdvds  13714  pcelnn  13783  xpsle  14360  isepi  14520  fthmon  14678  pospropd  15145  mndpropd  15287  grpidpropd  15288  mhmpropd  15310  grppropd  15394  ghmnsgima  15600  mndodcong  15789  odf1  15807  odf1o1  15815  sylow3lem6  15875  lsmcntzr  15921  efgredlema  15981  cmnpropd  16030  dprdf11  16196  rngpropd  16310  dvdsrpropd  16417  abvpropd  16546  lmodprop2d  16624  lsspropd  16712  lmhmpropd  16768  lbspropd  16794  lvecvscan  16806  lvecvscan2  16807  assapropd  17011  chrnzr  17436  zndvds0  17456  ip2eq  17509  phlpropd  17511  qtopcn  18761  tsmsf1o  19189  xmetgt0  19403  txmetcnp  19592  metustsymOLD  19606  metustsym  19607  nlmmul0or  19734  cnmet  19821  evth  19999  minveclem3b  20344  mbfposr  20557  itg2cn  20668  iblcnlem  20693  dvcvx  20919  ulm2  21316  efeq1  21451  dcubic  21707  mcubic  21708  dquart  21714  birthdaylem3  21813  ftalem2  21877  issqf  21940  sqff1o  21986  bposlem7  22095  lgsabs1  22139  lgsquadlem2  22160  dchrisum0lem1  22231  cusgra2v  22492  eupath2lem3  22722  nmounbi  23298  ip2eqi  23379  hvmulcan  23596  hvsubcan2  23599  hi2eq  23629  fh2  24144  riesz4i  24589  cvbr4i  24893  xdivpnfrp  25238  isorng  25428  ballotlemfc0  26025  ballotlemfcc  26026  sgnmulsgn  26082  sgnmulsgp  26083  subfacp1lem5  26218  divelunit  26524  mulcan1g  26528  cos2h  27604  tan2h  27605  dvasin  27660  topfneec2  27744  neibastop3  27763  caures  27838  ismtyima  27884  isdmn3  28056  rusbcALT  28867  infrglb  28948  climreeq  28964  sbc3orgOLD  30084  tendospcanN  33371  dochsncom  33730

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 179