MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr3d Structured version   Unicode version

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
StepHypRef Expression
1 3bitr3d.2 . . 3  |-  ( ph  ->  ( ps  <->  th )
)
2 3bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr3d 247 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
53, 4bitrd 245 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sbcne12g  3269  csbcomg  3274  ordsucuniel  4804  ordsucun  4805  eloprabga  6160  oeoa  6840  ereldm  6948  boxcutc  7105  mapen  7271  mapfien  7653  wemapwe  7654  sdom2en01  8182  prlem936  8924  subcan  9356  conjmul  9731  ltrec  9891  rebtwnz  10573  xposdif  10841  infmxrgelb  10913  fseq1m1p1  11123  fllt  11215  hashfacen  11703  hashf1  11706  lenegsq  12124  dvdsmod  12906  bitsmod  12948  smueqlem  13002  rpexp  13120  eulerthlem2  13171  odzdvds  13181  pcelnn  13243  xpsle  13806  isepi  13966  fthmon  14124  pospropd  14561  mndpropd  14721  grpidpropd  14722  mhmpropd  14744  grppropd  14823  ghmnsgima  15029  mndodcong  15180  odf1  15198  odf1o1  15206  sylow3lem6  15266  lsmcntzr  15312  efgredlema  15372  cmnpropd  15421  dprdf11  15581  rngpropd  15695  dvdsrpropd  15801  abvpropd  15930  lmodprop2d  16006  lsspropd  16093  lmhmpropd  16145  lbspropd  16171  lvecvscan  16183  lvecvscan2  16184  assapropd  16386  chrnzr  16811  zndvds0  16831  ip2eq  16884  phlpropd  16886  qtopcn  17746  tsmsf1o  18174  xmetgt0  18388  txmetcnp  18577  metustsymOLD  18591  metustsym  18592  nlmmul0or  18719  cnmet  18806  evth  18984  minveclem3b  19329  mbfposr  19544  itg2cn  19655  iblcnlem  19680  dvcvx  19904  ulm2  20301  efeq1  20431  dcubic  20686  mcubic  20687  dquart  20693  birthdaylem3  20792  ftalem2  20856  issqf  20919  sqff1o  20965  bposlem7  21074  lgsabs1  21118  lgsquadlem2  21139  dchrisum0lem1  21210  cusgra2v  21471  eupath2lem3  21701  nmounbi  22277  ip2eqi  22358  hvmulcan  22574  hvsubcan2  22577  hi2eq  22607  fh2  23121  riesz4i  23566  cvbr4i  23870  xdivpnfrp  24179  ballotlemfc0  24750  ballotlemfcc  24751  subfacp1lem5  24870  divelunit  25185  mulcan1g  25189  dvreasin  26290  topfneec2  26372  neibastop3  26391  caures  26466  ismtyima  26512  isdmn3  26684  rusbcALT  27616  infrglb  27698  climreeq  27715  sbc3org  28616  tendospcanN  31821  dochsncom  32180
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
  Copyright terms: Public domain W3C validator