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  3825  fnprb  6106  eloprabga  6362  ordsucuniel  6632  ordsucun  6633  oeoa  7238  ereldm  7347  boxcutc  7505  mapen  7674  mapfien  7859  mapfienOLD  8129  wemapwe  8130  wemapweOLD  8131  sdom2en01  8673  prlem936  9414  subcan  9865  mulcan1g  10198  conjmul  10257  ltrec  10421  rebtwnz  11182  xposdif  11457  infmxrgelb  11529  divelunit  11665  fseq1m1p1  11757  fzm1  11762  fllt  11924  hashfacen  12487  hashf1  12490  lenegsq  13235  dvdsmod  14127  bitsmod  14170  smueqlem  14224  rpexp  14345  eulerthlem2  14396  odzdvds  14406  pcelnn  14477  xpsle  15070  isepi  15228  fthmon  15415  pospropd  15963  grpidpropd  16087  mndpropd  16145  mhmpropd  16171  grppropd  16267  ghmnsgima  16489  mndodcong  16765  odf1  16783  odf1o1  16791  sylow3lem6  16851  lsmcntzr  16897  efgredlema  16957  cmnpropd  17006  dprdf11  17258  dprdf11OLD  17265  ringpropd  17425  dvdsrpropd  17540  abvpropd  17686  lmodprop2d  17767  lsspropd  17858  lmhmpropd  17914  lbspropd  17940  lvecvscan  17952  lvecvscan2  17953  assapropd  18171  chrnzr  18742  zndvds0  18762  ip2eq  18861  phlpropd  18863  qtopcn  20381  tsmsf1o  20813  xmetgt0  21027  txmetcnp  21216  metustsymOLD  21230  metustsym  21231  nlmmul0or  21358  cnmet  21445  evth  21625  minveclem3b  22009  mbfposr  22225  itg2cn  22336  iblcnlem  22361  dvcvx  22587  ulm2  22946  efeq1  23082  dcubic  23374  mcubic  23375  dquart  23381  birthdaylem3  23481  ftalem2  23545  issqf  23608  sqff1o  23654  bposlem7  23763  lgsabs1  23807  lgsquadlem2  23828  dchrisum0lem1  23899  opphllem6  24325  lmiinv  24359  cusgra2v  24664  eupath2lem3  25181  nmounbi  25889  ip2eqi  25970  hvmulcan  26187  hvsubcan2  26190  hi2eq  26220  fh2  26735  riesz4i  27180  cvbr4i  27484  xdivpnfrp  27863  isorng  28024  ballotlemfc0  28695  ballotlemfcc  28696  sgnmulsgn  28752  sgnmulsgp  28753  subfacp1lem5  28892  cos2h  30286  tan2h  30287  dvasin  30343  topfneec2  30414  neibastop3  30420  caures  30493  ismtyima  30539  isdmn3  30711  rusbcALT  31587  infrglb  31823  climreeq  31858  coseq0  31903  mgmhmpropd  32845  sbc3orgOLD  33693  tendospcanN  37147  dochsncom  37506