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  3701  sbcne12gOLD  3702  csbcomgOLD  3712  fnprb  5915  eloprabga  6149  ordsucuniel  6400  ordsucun  6401  oeoa  6952  ereldm  7060  boxcutc  7217  mapen  7383  mapfien  7765  wemapwe  7766  sdom2en01  8296  prlem936  9038  subcan  9482  conjmul  9862  ltrec  10022  rebtwnz  10759  xposdif  11032  infmxrgelb  11104  fseq1m1p1  11330  fllt  11448  hashfacen  11994  hashf1  11997  lenegsq  12594  dvdsmod  13376  bitsmod  13418  smueqlem  13472  rpexp  13592  eulerthlem2  13643  odzdvds  13653  pcelnn  13722  xpsle  14297  isepi  14457  fthmon  14615  pospropd  15082  mndpropd  15224  grpidpropd  15225  mhmpropd  15247  grppropd  15326  ghmnsgima  15532  mndodcong  15683  odf1  15701  odf1o1  15709  sylow3lem6  15769  lsmcntzr  15815  efgredlema  15875  cmnpropd  15924  dprdf11  16084  rngpropd  16198  dvdsrpropd  16304  abvpropd  16433  lmodprop2d  16509  lsspropd  16596  lmhmpropd  16648  lbspropd  16674  lvecvscan  16686  lvecvscan2  16687  assapropd  16889  chrnzr  17314  zndvds0  17334  ip2eq  17387  phlpropd  17389  qtopcn  18250  tsmsf1o  18678  xmetgt0  18892  txmetcnp  19081  metustsymOLD  19095  metustsym  19096  nlmmul0or  19223  cnmet  19310  evth  19488  minveclem3b  19833  mbfposr  20046  itg2cn  20157  iblcnlem  20182  dvcvx  20408  ulm2  20805  efeq1  20940  dcubic  21195  mcubic  21196  dquart  21202  birthdaylem3  21301  ftalem2  21365  issqf  21428  sqff1o  21474  bposlem7  21583  lgsabs1  21627  lgsquadlem2  21648  dchrisum0lem1  21719  cusgra2v  21980  eupath2lem3  22210  nmounbi  22786  ip2eqi  22867  hvmulcan  23084  hvsubcan2  23087  hi2eq  23117  fh2  23632  riesz4i  24077  cvbr4i  24381  xdivpnfrp  24729  isorng  24919  ballotlemfc0  25516  ballotlemfcc  25517  sgnmulsgn  25573  sgnmulsgp  25574  subfacp1lem5  25709  divelunit  26015  mulcan1g  26019  cos2h  27095  tan2h  27096  dvasin  27151  topfneec2  27235  neibastop3  27254  caures  27329  ismtyima  27375  isdmn3  27547  rusbcALT  28542  infrglb  28623  climreeq  28639  sbc3orgOLD  29807  tendospcanN  33094  dochsncom  33453

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