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

Theorem 3bitr2i 290
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1 (𝜑𝜓)
3bitr2i.2 (𝜒𝜓)
3bitr2i.3 (𝜒𝜃)
Assertion
Ref Expression
3bitr2i (𝜑𝜃)

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3 (𝜑𝜓)
2 3bitr2i.2 . . 3 (𝜒𝜓)
31, 2bitr4i 269 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 266 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  con2bi  344  an13  629  xorneg2  1628  2eu4  2731  2eu5  2732  exists1  2736  euxfr  3601  euind  3602  rmo4  3608  2reu5lem3  3624  rmo3  3734  difin  4074  reusv2lem4  5083  rabxp  5367  elvvv  5391  eliunxp  5474  elidinxp  5673  imadisj  5707  idrefALT  5732  intirr  5738  resco  5866  funcnv3  6179  fncnv  6182  fun11  6183  fununi  6184  mptfnf  6235  f1mpt  6751  mpt2mptx  6990  uniuni  7210  frxp  7530  oeeu  7929  ixp0x  8182  xpcomco  8298  1sdom  8411  dffi3  8585  wemapsolem  8703  cardval3  9070  kmlem4  9269  kmlem12  9277  kmlem14  9279  kmlem15  9280  kmlem16  9281  fpwwe2  9759  axgroth4  9948  ltexprlem4  10155  bitsmod  15396  pythagtrip  15775  isstruct  16100  pgpfac1  18700  pgpfac  18704  isassa  19543  basdif0  20991  ntreq0  21115  tgcmp  21438  tx1cn  21646  rnelfmlem  21989  phtpcer  23027  iscvsp  23160  caucfil  23314  minveclem1  23429  ovoliunlem1  23505  mdegleb  24060  istrkg2ld  25595  numedglnl  26276  usgr2pth0  26911  adjbd1o  29294  nmo  29675  rmo3f  29683  rmo4fOLD  29684  difrab2  29686  mpt2mptxf  29826  isros  30578  1stmbfm  30669  bnj976  31192  bnj1143  31205  bnj1533  31266  bnj864  31336  bnj983  31365  bnj1174  31415  bnj1175  31416  bnj1280  31432  cvmlift2lem12  31640  axacprim  31927  dmscut  32260  dfrecs2  32399  andnand1  32738  bj-dfssb2  32976  bj-denotes  33183  bj-snglc  33285  bj-disj2r  33341  bj-dfmpt2a  33400  bj-mpt2mptALT  33401  mptsnunlem  33520  wl-cases2-dnf  33629  itg2addnc  33794  asindmre  33825  brres2  34370  brxrn2  34468  dfxrn2  34469  inxpxrn  34484  refsymrel2  34644  refsymrel3  34645  isopos  34978  dihglblem6  37138  dihglb2  37140  fgraphopab  38306  ifpid2g  38355  ifpim23g  38357  rp-fakeanorass  38375  elmapintrab  38399  relintabex  38404  relnonrel  38410  undmrnresiss  38427  elintima  38462  relexp0eq  38510  iunrelexp0  38511  dffrege115  38789  frege131  38805  frege133  38807  ntrneikb  38909  onfrALTlem5  39272  onfrALTlem5VD  39632  ndisj2  39728  ndmaovcom  41811  eliunxp2  42697  mpt2mptx2  42698  alimp-no-surprise  43115  alsi-no-surprise  43130
  Copyright terms: Public domain W3C validator