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

Theorem 3bitr2i 288
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 267 . 2 (𝜑𝜒)
4 3bitr2i.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:  con2bi  343  an13  840  xorneg2  1473  2eu4  2555  2eu5  2556  exists1  2560  euxfr  3390  euind  3391  rmo4  3397  2reu5lem3  3413  rmo3  3526  difin  3859  reusv2lem4  4870  rabxp  5152  elvvv  5176  eliunxp  5257  imadisj  5482  intirr  5512  resco  5637  funcnv3  5957  fncnv  5960  fun11  5961  fununi  5962  mptfnf  6013  f1mpt  6515  mpt2mptx  6748  uniuni  6968  frxp  7284  oeeu  7680  ixp0x  7933  mapsnen  8032  xpcomco  8047  1sdom  8160  dffi3  8334  wemapsolem  8452  cardval3  8775  kmlem4  8972  kmlem12  8980  kmlem14  8982  kmlem15  8983  kmlem16  8984  fpwwe2  9462  axgroth4  9651  ltexprlem4  9858  bitsmod  15152  pythagtrip  15533  pgpfac1  18473  pgpfac  18477  isassa  19309  basdif0  20751  ntreq0  20875  tgcmp  21198  tx1cn  21406  rnelfmlem  21750  phtpcer  22788  phtpcerOLD  22789  iscvsp  22922  caucfil  23075  minveclem1  23189  ovoliunlem1  23264  mdegleb  23818  istrkg2ld  25353  numedglnl  26033  usgr2pth0  26655  adjbd1o  28928  nmo  29309  rmo3f  29319  rmo4fOLD  29320  difrab2  29323  mpt2mptxf  29462  isros  30216  1stmbfm  30307  bnj976  30833  bnj1143  30846  bnj1533  30907  bnj864  30977  bnj983  31006  bnj1174  31056  bnj1175  31057  bnj1280  31073  cvmlift2lem12  31281  axacprim  31569  dmscut  31902  dfrecs2  32041  andnand1  32382  bj-dfssb2  32624  bj-denotes  32842  bj-snglc  32941  bj-disj2r  32997  bj-dfmpt2a  33055  bj-mpt2mptALT  33056  mptsnunlem  33165  wl-cases2-dnf  33275  itg2addnc  33444  asindmre  33475  isopos  34293  dihglblem6  36455  dihglb2  36457  fgraphopab  37614  ifpid2g  37664  ifpim23g  37666  rp-fakeanorass  37684  elmapintrab  37708  relintabex  37713  relnonrel  37719  undmrnresiss  37736  elintima  37771  relexp0eq  37819  iunrelexp0  37820  dffrege115  38098  frege131  38114  frege133  38116  ntrneikb  38218  onfrALTlem5  38583  ndisj2  39044  ndmaovcom  41054  eliunxp2  41883  mpt2mptx2  41884  alimp-no-surprise  42298  alsi-no-surprise  42313
  Copyright terms: Public domain W3C validator