Theorem 3bitr3d 275

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	|- ( ph -> ( ps <-> ch ) )
3bitr3d.2	|- ( ph -> ( ps <-> th ) )
3bitr3d.3	|- ( ph -> ( ch <-> ta ) )

Assertion

Ref	Expression
3bitr3d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 |- ( ph -> ( ps <-> th ) )
2		3bitr3d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr3d 247	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 245	1 |- ( ph -> ( th <-> ta ) )

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

This theorem is referenced by:  sbcne12g  3229  csbcomg  3234  ordsucuniel  4763  ordsucun  4764  eloprabga  6119  oeoa  6799  ereldm  6907  boxcutc  7064  mapen  7230  mapfien  7609  wemapwe  7610  sdom2en01  8138  prlem936  8880  subcan  9312  conjmul  9687  ltrec  9847  rebtwnz  10529  xposdif  10797  infmxrgelb  10869  fseq1m1p1  11078  fllt  11170  hashfacen  11658  hashf1  11661  lenegsq  12079  dvdsmod  12861  bitsmod  12903  smueqlem  12957  rpexp  13075  eulerthlem2  13126  odzdvds  13136  pcelnn  13198  xpsle  13761  isepi  13921  fthmon  14079  pospropd  14516  mndpropd  14676  grpidpropd  14677  mhmpropd  14699  grppropd  14778  ghmnsgima  14984  mndodcong  15135  odf1  15153  odf1o1  15161  sylow3lem6  15221  lsmcntzr  15267  efgredlema  15327  cmnpropd  15376  dprdf11  15536  rngpropd  15650  dvdsrpropd  15756  abvpropd  15885  lmodprop2d  15961  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  lvecvscan  16138  lvecvscan2  16139  assapropd  16341  chrnzr  16766  zndvds0  16786  ip2eq  16839  phlpropd  16841  qtopcn  17699  tsmsf1o  18127  xmetgt0  18341  txmetcnp  18530  metustsymOLD  18544  metustsym  18545  nlmmul0or  18672  cnmet  18759  evth  18937  minveclem3b  19282  mbfposr  19497  itg2cn  19608  iblcnlem  19633  dvcvx  19857  ulm2  20254  efeq1  20384  dcubic  20639  mcubic  20640  dquart  20646  birthdaylem3  20745  ftalem2  20809  issqf  20872  sqff1o  20918  bposlem7  21027  lgsabs1  21071  lgsquadlem2  21092  dchrisum0lem1  21163  cusgra2v  21424  eupath2lem3  21654  nmounbi  22230  ip2eqi  22311  hvmulcan  22527  hvsubcan2  22530  hi2eq  22560  fh2  23074  riesz4i  23519  cvbr4i  23823  xdivpnfrp  24132  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem5  24823  divelunit  25138  mulcan1g  25142  dvreasin  26179  topfneec2  26262  neibastop3  26281  caures  26356  ismtyima  26402  isdmn3  26574  rusbcALT  27507  infrglb  27589  climreeq  27606  sbc3org  28327  tendospcanN  31506  dochsncom  31865

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178