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

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  |-  ( 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 248 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
53, 4bitrd 246 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  sbcne12g  3271  csbcomg  3276  ordsucuniel  4807  ordsucun  4808  eloprabga  6163  oeoa  6843  ereldm  6951  boxcutc  7108  mapen  7274  mapfien  7656  wemapwe  7657  sdom2en01  8187  prlem936  8929  subcan  9361  conjmul  9736  ltrec  9896  rebtwnz  10578  xposdif  10846  infmxrgelb  10918  fseq1m1p1  11128  fllt  11220  hashfacen  11708  hashf1  11711  lenegsq  12129  dvdsmod  12911  bitsmod  12953  smueqlem  13007  rpexp  13125  eulerthlem2  13176  odzdvds  13186  pcelnn  13248  xpsle  13811  isepi  13971  fthmon  14129  pospropd  14566  mndpropd  14726  grpidpropd  14727  mhmpropd  14749  grppropd  14828  ghmnsgima  15034  mndodcong  15185  odf1  15203  odf1o1  15211  sylow3lem6  15271  lsmcntzr  15317  efgredlema  15377  cmnpropd  15426  dprdf11  15586  rngpropd  15700  dvdsrpropd  15806  abvpropd  15935  lmodprop2d  16011  lsspropd  16098  lmhmpropd  16150  lbspropd  16176  lvecvscan  16188  lvecvscan2  16189  assapropd  16391  chrnzr  16816  zndvds0  16836  ip2eq  16889  phlpropd  16891  qtopcn  17751  tsmsf1o  18179  xmetgt0  18393  txmetcnp  18582  metustsymOLD  18596  metustsym  18597  nlmmul0or  18724  cnmet  18811  evth  18989  minveclem3b  19334  mbfposr  19547  itg2cn  19658  iblcnlem  19683  dvcvx  19909  ulm2  20306  efeq1  20436  dcubic  20691  mcubic  20692  dquart  20698  birthdaylem3  20797  ftalem2  20861  issqf  20924  sqff1o  20970  bposlem7  21079  lgsabs1  21123  lgsquadlem2  21144  dchrisum0lem1  21215  cusgra2v  21476  eupath2lem3  21706  nmounbi  22282  ip2eqi  22363  hvmulcan  22579  hvsubcan2  22582  hi2eq  22612  fh2  23126  riesz4i  23571  cvbr4i  23875  xdivpnfrp  24184  ballotlemfc0  24755  ballotlemfcc  24756  subfacp1lem5  24875  divelunit  25190  mulcan1g  25194  cos2h  26251  tan2h  26252  dvreasin  26303  topfneec2  26385  neibastop3  26404  caures  26479  ismtyima  26525  isdmn3  26697  rusbcALT  27629  infrglb  27711  climreeq  27728  sbc3org  28689  tendospcanN  31894  dochsncom  32253
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
  Copyright terms: Public domain W3C validator