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  342  an13  857  xorneg2  1514  2eu4  2585  2eu5  2586  exists1  2590  euxfr  3425  euind  3426  rmo4  3432  2reu5lem3  3448  rmo3  3561  difin  3894  reusv2lem4  4902  rabxp  5188  elvvv  5212  eliunxp  5292  imadisj  5519  intirr  5549  resco  5677  funcnv3  5997  fncnv  6000  fun11  6001  fununi  6002  mptfnf  6053  f1mpt  6558  mpt2mptx  6793  uniuni  7013  frxp  7332  oeeu  7728  ixp0x  7978  mapsnen  8076  xpcomco  8091  1sdom  8204  dffi3  8378  wemapsolem  8496  cardval3  8816  kmlem4  9013  kmlem12  9021  kmlem14  9023  kmlem15  9024  kmlem16  9025  fpwwe2  9503  axgroth4  9692  ltexprlem4  9899  bitsmod  15205  pythagtrip  15586  pgpfac1  18525  pgpfac  18529  isassa  19363  basdif0  20805  ntreq0  20929  tgcmp  21252  tx1cn  21460  rnelfmlem  21803  phtpcer  22841  iscvsp  22974  caucfil  23127  minveclem1  23241  ovoliunlem1  23316  mdegleb  23869  istrkg2ld  25404  numedglnl  26084  usgr2pth0  26717  adjbd1o  29072  nmo  29453  rmo3f  29462  rmo4fOLD  29463  difrab2  29465  mpt2mptxf  29605  isros  30359  1stmbfm  30450  bnj976  30974  bnj1143  30987  bnj1533  31048  bnj864  31118  bnj983  31147  bnj1174  31197  bnj1175  31198  bnj1280  31214  cvmlift2lem12  31422  axacprim  31710  dmscut  32043  dfrecs2  32182  andnand1  32523  bj-dfssb2  32765  bj-denotes  32983  bj-snglc  33082  bj-disj2r  33138  bj-dfmpt2a  33196  bj-mpt2mptALT  33197  mptsnunlem  33315  wl-cases2-dnf  33425  itg2addnc  33594  asindmre  33625  brres2  34176  brxrn2  34277  dfxrn2  34278  inxpxrn  34293  refsymrel2  34451  refsymrel3  34452  isopos  34785  dihglblem6  36946  dihglb2  36948  fgraphopab  38105  ifpid2g  38155  ifpim23g  38157  rp-fakeanorass  38175  elmapintrab  38199  relintabex  38204  relnonrel  38210  undmrnresiss  38227  elintima  38262  relexp0eq  38310  iunrelexp0  38311  dffrege115  38589  frege131  38605  frege133  38607  ntrneikb  38709  onfrALTlem5  39074  onfrALTlem5VD  39435  ndisj2  39532  ndmaovcom  41606  eliunxp2  42437  mpt2mptx2  42438  alimp-no-surprise  42855  alsi-no-surprise  42870
  Copyright terms: Public domain W3C validator