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

Theorem 3bitr4rd 286
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3bitr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3bitr4rd  |-  ( ph  ->  ( ta  <->  th )
)

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr4d 256 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 256 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff setvar class
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:  inimasn  5249  oacan  6979  ecdmn0  7135  wemapwe  7920  wemapweOLD  7921  r1pw  8044  adderpqlem  9115  mulerpqlem  9116  lterpq  9131  ltanq  9132  genpass  9170  readdcan  9535  lemuldiv  10203  msq11  10225  avglt2  10555  qbtwnre  11161  iooshf  11366  clim2c  12975  lo1o1  13002  climabs0  13055  reef11  13395  absefib  13474  efieq1re  13475  pc2dvds  13937  pcmpt  13946  subsubc  14755  odmulgid  16046  gexdvds  16074  submcmn2  16314  obslbs  18135  cnntr  18859  cndis  18875  cnindis  18876  cnpdis  18877  lmres  18884  cmpfi  18991  ist0-4  19282  txhmeo  19356  tsmssubm  19696  blin  19976  cncfmet  20464  icopnfcnv  20494  lmmbrf  20753  iscauf  20771  causs  20789  mbfposr  21110  itg2gt0  21218  limcflf  21336  limcres  21341  lhop1  21466  dvdsr1p  21613  fsumvma2  22533  vmasum  22535  chpchtsum  22538  bposlem1  22603  iscgrgd  22946  lnrot1  23010  eqeelen  23118  nbgraeledg  23309  nb3graprlem2  23328  cusgra3v  23340  cusgrauvtxb  23372  dmdmd  25672  funcnvmptOLD  25954  funcnvmpt  25955  xrdifh  26038  eulerpartlemgh  26730  signslema  26932  leceifl  28391  iblabsnclem  28426  ftc1anclem6  28443  areacirclem5  28459  areacirc  28460  ellz1  29076  islssfg  29394  proot1ex  29540  el2spthonot0  30361  clwlkisclwwlk2  30423  rusgranumwlks  30545  lsatfixedN  32547  cdlemg10c  34176  diaglbN  34593  dih1  34824  dihglbcpreN  34838  mapdcv  35198
  Copyright terms: Public domain W3C validator