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

Theorem 3bitr2i 286
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 265 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 262 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  con2bi  341  an13  835  xorneg2  1465  2eu4  2539  2eu5  2540  exists1  2544  euxfr  3354  euind  3355  rmo4  3361  2reu5lem3  3377  rmo3  3489  difin  3818  reusv2lem4  4789  rabxp  5064  elvvv  5087  eliunxp  5165  imadisj  5386  intirr  5416  resco  5538  funcnv3  5855  fncnv  5858  fun11  5859  fununi  5860  mptfnf  5910  f1mpt  6393  mpt2mptx  6623  uniuni  6838  frxp  7147  oeeu  7543  ixp0x  7795  mapsnen  7893  xpcomco  7908  1sdom  8021  dffi3  8193  wemapsolem  8311  cardval3  8634  kmlem4  8831  kmlem12  8839  kmlem14  8841  kmlem15  8842  kmlem16  8843  fpwwe2  9317  axgroth4  9506  ltexprlem4  9713  bitsmod  14938  pythagtrip  15319  pgpfac1  18244  pgpfac  18248  isassa  19078  basdif0  20506  ntreq0  20629  tgcmp  20952  tx1cn  21160  rnelfmlem  21504  phtpcer  22529  phtpcerOLD  22530  iscvsp  22661  caucfil  22803  minveclem1  22916  ovoliunlem1  22990  mdegleb  23541  istrkg2ld  25072  3v3e3cycl2  25954  iswwlk  25973  adjbd1o  28130  nmo  28511  rmo3f  28521  rmo4fOLD  28522  mpt2mptxf  28662  isros  29360  1stmbfm  29451  bnj976  29904  bnj1143  29917  bnj1533  29978  bnj864  30048  bnj983  30077  bnj1174  30127  bnj1175  30128  bnj1280  30144  cvmlift2lem12  30352  axacprim  30640  dfrecs2  31029  andnand1  31370  bj-dfssb2  31631  bj-denotes  31851  bj-snglc  31949  bj-dfmpt2a  32051  bj-mpt2mptALT  32052  mptsnunlem  32160  wl-cases2-dnf  32273  itg2addnc  32433  asindmre  32464  isopos  33284  dihglblem6  35446  dihglb2  35448  fgraphopab  36606  ifpid2g  36656  ifpim23g  36658  rp-fakeanorass  36676  elmapintrab  36700  relintabex  36705  relnonrel  36711  undmrnresiss  36728  elintima  36763  relexp0eq  36811  iunrelexp0  36812  dffrege115  37091  frege131  37107  frege133  37109  ntrneikb  37211  onfrALTlem5  37577  ndisj2  38042  ndmaovcom  39735  usgr2pth0  40969  eliunxp2  41903  mpt2mptx2  41904  alimp-no-surprise  42295  alsi-no-surprise  42310
  Copyright terms: Public domain W3C validator