Theorem 3bitr3d 283

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

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

This theorem is referenced by:  sbcne12  3827  sbcne12gOLD  3828  csbcomgOLD  3838  fnprb  6129  eloprabga  6389  ordsucuniel  6659  ordsucun  6660  oeoa  7265  ereldm  7374  boxcutc  7532  mapen  7701  mapfien  7887  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  sdom2en01  8703  prlem936  9446  subcan  9897  mulcan1g  10227  conjmul  10286  ltrec  10451  rebtwnz  11210  xposdif  11483  infmxrgelb  11555  divelunit  11691  fseq1m1p1  11782  fzm1  11787  fllt  11943  hashfacen  12503  hashf1  12506  lenegsq  13153  dvdsmod  14043  bitsmod  14086  smueqlem  14140  rpexp  14261  eulerthlem2  14312  odzdvds  14322  pcelnn  14393  xpsle  14978  isepi  15135  fthmon  15296  pospropd  15764  grpidpropd  15888  mndpropd  15946  mhmpropd  15972  grppropd  16068  ghmnsgima  16290  mndodcong  16566  odf1  16584  odf1o1  16592  sylow3lem6  16652  lsmcntzr  16698  efgredlema  16758  cmnpropd  16807  dprdf11  17063  dprdf11OLD  17070  ringpropd  17230  dvdsrpropd  17345  abvpropd  17491  lmodprop2d  17572  lsspropd  17663  lmhmpropd  17719  lbspropd  17745  lvecvscan  17757  lvecvscan2  17758  assapropd  17976  chrnzr  18567  zndvds0  18589  ip2eq  18688  phlpropd  18690  qtopcn  20215  tsmsf1o  20647  xmetgt0  20861  txmetcnp  21050  metustsymOLD  21064  metustsym  21065  nlmmul0or  21192  cnmet  21279  evth  21459  minveclem3b  21843  mbfposr  22059  itg2cn  22170  iblcnlem  22195  dvcvx  22421  ulm2  22780  efeq1  22916  dcubic  23177  mcubic  23178  dquart  23184  birthdaylem3  23283  ftalem2  23347  issqf  23410  sqff1o  23456  bposlem7  23565  lgsabs1  23609  lgsquadlem2  23630  dchrisum0lem1  23701  opphllem6  24124  lmiinv  24158  cusgra2v  24462  eupath2lem3  24979  nmounbi  25691  ip2eqi  25772  hvmulcan  25989  hvsubcan2  25992  hi2eq  26022  fh2  26537  riesz4i  26982  cvbr4i  27286  xdivpnfrp  27629  isorng  27789  ballotlemfc0  28431  ballotlemfcc  28432  sgnmulsgn  28488  sgnmulsgp  28489  subfacp1lem5  28628  cos2h  30046  tan2h  30047  dvasin  30103  topfneec2  30174  neibastop3  30180  caures  30253  ismtyima  30299  isdmn3  30471  rusbcALT  31346  infrglb  31584  climreeq  31619  coseq0  31664  mgmhmpropd  32473  sbc3orgOLD  33303  tendospcanN  36750  dochsncom  37109

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 185