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	|- ( 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 255	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 253	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem is referenced by:  sbcne12  3780  sbcne12gOLD  3781  csbcomgOLD  3791  fnprb  6038  eloprabga  6280  ordsucuniel  6538  ordsucun  6539  oeoa  7139  ereldm  7247  boxcutc  7409  mapen  7578  mapfien  7761  mapfienOLD  8031  wemapwe  8032  wemapweOLD  8033  sdom2en01  8575  prlem936  9320  subcan  9768  mulcan1g  10093  conjmul  10152  ltrec  10317  rebtwnz  11056  xposdif  11329  infmxrgelb  11401  divelunit  11537  fseq1m1p1  11645  fllt  11766  hashfacen  12318  hashf1  12321  lenegsq  12919  dvdsmod  13701  bitsmod  13743  smueqlem  13797  rpexp  13917  eulerthlem2  13968  odzdvds  13978  pcelnn  14047  xpsle  14630  isepi  14790  fthmon  14948  pospropd  15415  mndpropd  15557  grpidpropd  15558  mhmpropd  15581  grppropd  15667  ghmnsgima  15881  mndodcong  16158  odf1  16176  odf1o1  16184  sylow3lem6  16244  lsmcntzr  16290  efgredlema  16350  cmnpropd  16399  dprdf11  16627  dprdf11OLD  16634  rngpropd  16791  dvdsrpropd  16903  abvpropd  17042  lmodprop2d  17122  lsspropd  17213  lmhmpropd  17269  lbspropd  17295  lvecvscan  17307  lvecvscan2  17308  assapropd  17513  chrnzr  18079  zndvds0  18101  ip2eq  18200  phlpropd  18202  qtopcn  19412  tsmsf1o  19844  xmetgt0  20058  txmetcnp  20247  metustsymOLD  20261  metustsym  20262  nlmmul0or  20389  cnmet  20476  evth  20656  minveclem3b  21040  mbfposr  21256  itg2cn  21367  iblcnlem  21392  dvcvx  21618  ulm2  21976  efeq1  22111  dcubic  22367  mcubic  22368  dquart  22374  birthdaylem3  22473  ftalem2  22537  issqf  22600  sqff1o  22646  bposlem7  22755  lgsabs1  22799  lgsquadlem2  22820  dchrisum0lem1  22891  cusgra2v  23515  eupath2lem3  23745  nmounbi  24321  ip2eqi  24402  hvmulcan  24619  hvsubcan2  24622  hi2eq  24652  fh2  25167  riesz4i  25612  cvbr4i  25916  xdivpnfrp  26246  isorng  26405  ballotlemfc0  27012  ballotlemfcc  27013  sgnmulsgn  27069  sgnmulsgp  27070  subfacp1lem5  27209  cos2h  28564  tan2h  28565  dvasin  28621  topfneec2  28705  neibastop3  28724  caures  28797  ismtyima  28843  isdmn3  29015  rusbcALT  29834  infrglb  29912  climreeq  29927  sbc3orgOLD  31541  tendospcanN  34977  dochsncom  35336