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  3661  sbcne12gOLD  3662  csbcomgOLD  3672  ordsucuniel  4849  ordsucun  4850  eloprabga  6214  oeoa  6893  ereldm  7001  boxcutc  7158  mapen  7324  mapfien  7706  wemapwe  7707  sdom2en01  8237  prlem936  8979  subcan  9411  conjmul  9786  ltrec  9946  rebtwnz  10628  xposdif  10896  infmxrgelb  10968  fseq1m1p1  11178  fllt  11270  hashfacen  11758  hashf1  11761  lenegsq  12179  dvdsmod  12961  bitsmod  13003  smueqlem  13057  rpexp  13175  eulerthlem2  13226  odzdvds  13236  pcelnn  13298  xpsle  13861  isepi  14021  fthmon  14179  pospropd  14616  mndpropd  14757  grpidpropd  14758  mhmpropd  14780  grppropd  14859  ghmnsgima  15065  mndodcong  15216  odf1  15234  odf1o1  15242  sylow3lem6  15302  lsmcntzr  15348  efgredlema  15408  cmnpropd  15457  dprdf11  15617  rngpropd  15731  dvdsrpropd  15837  abvpropd  15966  lmodprop2d  16042  lsspropd  16129  lmhmpropd  16181  lbspropd  16207  lvecvscan  16219  lvecvscan2  16220  assapropd  16422  chrnzr  16847  zndvds0  16867  ip2eq  16920  phlpropd  16922  qtopcn  17782  tsmsf1o  18210  xmetgt0  18424  txmetcnp  18613  metustsymOLD  18627  metustsym  18628  nlmmul0or  18755  cnmet  18842  evth  19020  minveclem3b  19365  mbfposr  19578  itg2cn  19689  iblcnlem  19714  dvcvx  19940  ulm2  20337  efeq1  20467  dcubic  20722  mcubic  20723  dquart  20729  birthdaylem3  20828  ftalem2  20892  issqf  20955  sqff1o  21001  bposlem7  21110  lgsabs1  21154  lgsquadlem2  21175  dchrisum0lem1  21246  cusgra2v  21507  eupath2lem3  21737  nmounbi  22313  ip2eqi  22394  hvmulcan  22610  hvsubcan2  22613  hi2eq  22643  fh2  23157  riesz4i  23602  cvbr4i  23906  xdivpnfrp  24255  isorng  24432  ballotlemfc0  25010  ballotlemfcc  25011  subfacp1lem5  25130  divelunit  25445  mulcan1g  25449  cos2h  26504  tan2h  26505  dvreasin  26557  topfneec2  26639  neibastop3  26658  caures  26733  ismtyima  26779  isdmn3  26951  rusbcALT  27951  infrglb  28032  climreeq  28049  sbc3orgOLD  29011  tendospcanN  32217  dochsncom  32576

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