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

Theorem 3bitr3i 275
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1
3bitr3i.2
3bitr3i.3
Assertion
Ref Expression
3bitr3i

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3
2 3bitr3i.1 . . 3
31, 2bitr3i 251 . 2
4 3bitr3i.3 . 2
53, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  an12  797  19.35OLD  1688  cbval2  2027  cbvex2OLD  2029  sbco2d  2159  sbcom  2161  equsb3  2176  equsb3ALT  2177  elsb3  2178  elsb4  2179  sb7f  2197  sbco4lem  2209  eq2tri  2525  eqsb3  2577  clelsb3  2578  r19.35  3004  ralcom4  3128  rexcom4  3129  ceqsralt  3133  gencbvex  3153  gencbval  3155  ceqsrexbv  3234  euind  3286  reuind  3303  sbccomlem  3406  sbccom  3407  csbcom  3837  difcom  3912  uniintsn  4324  disjxun  4450  reusv2lem4  4656  exss  4715  elxp2  5022  eqbrriv  5103  dm0rn0  5224  dfres2  5331  qfto  5393  rninxp  5451  coeq0  5521  fununi  5659  dffv2  5946  fndmin  5994  fnprb  6129  dfoprab2  6343  dfer2  7331  eceqoveq  7435  euen1  7605  xpsnen  7621  xpassen  7631  marypha2lem3  7917  rankuni  8302  card1  8370  alephislim  8485  dfacacn  8542  kmlem4  8554  ac6num  8880  zorn2lem4  8900  fpwwe2lem8  9036  fpwwe2lem12  9040  mappsrpr  9506  sqeqori  12280  vdwmc2  14497  txflf  20507  metustidOLD  21062  metustid  21063  caucfil  21722  ovolgelb  21891  axcontlem5  24271  nmoubi  25687  hvsubaddi  25983  hlimeui  26158  omlsilem  26320  pjoml3i  26504  hodsi  26694  nmopub  26827  nmfnleub  26844  nmopcoadj0i  27022  pjin3i  27113  or3dir  27368  ralcom4f  27375  rexcom4f  27376  clelsb3f  27379  uniinn0  27424  ordtconlem1  27906  br1steq  29204  br2ndeq  29205  elima4  29209  brfullfun  29598  filnetlem4  30199  sbccom2lem  30529  moxfr  30624  hashnzfzclim  31227  pm11.6  31298  fprodle  31604  copisnmnd  32497  sbc3or  33302  cbvexsv  33319  bnj62  33773  bnj610  33804  bnj1143  33849  bnj1533  33910  bnj543  33951  bnj545  33953  bnj594  33970  bj-cbval2v  34302  bj-clelsb3  34424  isltrn2N  35844  bj-iforcor  37724  trclubg  37785  frege72  37963
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
  Copyright terms: Public domain W3C validator