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

Theorem 3bitr3i 304
 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 280 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 278 1 (𝜒𝜃)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209 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 210 This theorem is referenced by:  an33rean  1480  xorass  1507  cbvaldvaw  2045  sbievw2  2104  sbco4lem  2279  cbval2vOLD  2353  cbvex  2406  cbvexvOLD  2410  cbval2OLD  2422  sbco2d  2531  sbcom  2533  sb7f  2545  sb7fALT  2592  eq2tri  2860  clelsb3vOLD  2918  clelsb3fw  2959  clelsb3f  2960  cbvraldva2  3403  cbvrexdva2  3404  cbvrexdva2OLD  3405  ralcom4OLD  3472  rexcom4OLD  3473  ceqsralt  3475  gencbvex  3497  gencbval  3499  ceqsrexbv  3598  euind  3663  reuind  3692  sbccomlem  3799  sbccom  3800  csbcom  4325  difcom  4392  eqsn  4722  uniintsn  4876  disjxun  5029  reusv2lem4  5268  exss  5321  opab0  5407  opelinxp  5596  eqbrriv  5629  dm0rn0  5760  elidinxp  5879  qfto  5949  rninxp  6004  coeq0  6076  fununi  6400  dffv2  6734  fndmin  6793  fnprb  6949  fntpb  6950  dfoprab2  7192  dfer2  8276  eceqoveq  8388  euen1  8565  xpsnen  8587  xpassen  8597  marypha2lem3  8888  rankuni  9279  card1  9384  alephislim  9497  dfacacn  9555  kmlem4  9567  ac6num  9893  zorn2lem4  9913  mappsrpr  10522  sqeqori  13575  trclublem  14349  fprodle  15345  vdwmc2  16308  txflf  22621  metustid  23171  caucfil  23897  ovolgelb  24094  dfcgra2  26634  axcontlem5  26772  frgr3v  28070  nmoubi  28565  hvsubaddi  28859  hlimeui  29033  omlsilem  29195  pjoml3i  29379  hodsi  29568  nmopub  29701  nmfnleub  29718  nmopcoadj0i  29896  pjin3i  29987  or3dir  30242  ralcom4f  30250  rexcom4f  30251  uniinn0  30324  ordtconnlem1  31292  bnj62  32115  bnj610  32143  bnj1143  32187  bnj1533  32249  bnj543  32290  bnj545  32292  bnj594  32309  cusgracyclt3v  32531  ceqsralv2  33084  brsuccf  33530  brfullfun  33537  filnetlem4  33857  icorempo  34787  poimirlem13  35089  poimirlem14  35090  poimirlem21  35097  poimirlem22  35098  poimir  35109  sbccom2lem  35581  alrmomorn  35791  dfeldisj5  36133  isltrn2N  37435  moxfr  39676  ifporcor  40213  ifpancor  40215  ifpbicor  40226  ifpnorcor  40231  ifpnancor  40232  ifpororb  40256  relexp0eq  40445  hashnzfzclim  41069  pm11.6  41139  sbc3or  41281  cbvexsv  41296  dfich2  44018  ichbi12i  44020  sprvalpwn0  44043  copisnmnd  44472
 Copyright terms: Public domain W3C validator