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

Theorem 3bitr3i 290
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 266 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 264 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  an12  837  xorass  1465  cbval2  2278  cbvaldva  2280  sbco2d  2415  sbcom  2417  equsb3  2431  equsb3ALT  2432  elsb3  2433  elsb4  2434  sb7f  2452  sbco4lem  2464  eq2tri  2682  eqsb3  2725  clelsb3  2726  r19.35  3078  ralcom4  3214  rexcom4  3215  ceqsralt  3219  gencbvex  3240  gencbval  3242  ceqsrexbv  3325  euind  3380  reuind  3398  sbccomlem  3495  sbccom  3496  csbcom  3972  difcom  4031  eqsn  4336  uniintsn  4486  disjxun  4621  reusv2lem4  4842  exss  4902  opab0  4977  elxp2OLD  5103  eqbrriv  5186  dm0rn0  5312  dfres2  5422  qfto  5486  rninxp  5542  coeq0  5613  fununi  5932  dffv2  6238  fndmin  6290  fnprb  6437  fntpb  6438  dfoprab2  6666  dfer2  7703  eceqoveq  7813  euen1  7986  xpsnen  8004  xpassen  8014  marypha2lem3  8303  rankuni  8686  card1  8754  alephislim  8866  dfacacn  8923  kmlem4  8935  ac6num  9261  zorn2lem4  9281  fpwwe2lem8  9419  fpwwe2lem12  9423  mappsrpr  9889  sqeqori  12932  trclublem  13684  fprodle  14671  vdwmc2  15626  txflf  21750  metustid  22299  caucfil  23021  ovolgelb  23188  dfcgra2  25655  axcontlem5  25782  frgr3v  27037  nmoubi  27515  hvsubaddi  27811  hlimeui  27985  omlsilem  28149  pjoml3i  28333  hodsi  28522  nmopub  28655  nmfnleub  28672  nmopcoadj0i  28850  pjin3i  28941  or3dir  29196  ralcom4f  29204  rexcom4f  29205  clelsb3f  29209  uniinn0  29253  ordtconnlem1  29794  bnj62  30547  bnj610  30578  bnj1143  30622  bnj1533  30683  bnj543  30724  bnj545  30726  bnj594  30743  ceqsralv2  31369  br1steq  31427  br2ndeq  31428  brsuccf  31743  brfullfun  31750  filnetlem4  32071  bj-ssbcom3lem  32345  bj-cbval2v  32432  bj-clelsb3  32548  icorempt2  32870  poimirlem13  33093  poimirlem14  33094  poimirlem21  33101  poimirlem22  33102  poimir  33113  sbccom2lem  33600  isltrn2N  34925  moxfr  36774  ifporcor  37326  ifpancor  37328  ifpbicor  37340  ifpnorcor  37345  ifpnancor  37346  ifpororb  37370  relexp0eq  37513  hashnzfzclim  38042  pm11.6  38113  sbc3or  38259  cbvexsv  38283  sprvalpwn0  41051  copisnmnd  41127
  Copyright terms: Public domain W3C validator