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

Theorem 3bitr2i 300
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 279 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 276 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  con2bi  355  xorneg2  1505  sbrimvlem  2092  dfsb7OLD  2278  2eu4  2737  2eu5  2738  2eu5OLD  2739  euxfrw  3711  euxfr  3713  euind  3714  rmo4  3720  rmo3f  3724  2reu5lem3  3747  rmo3  3871  rmo3OLD  3872  difin  4237  axsepgfromrep  5193  reusv2lem4  5293  rabxp  5594  elvvv  5621  eliunxp  5702  elidinxp  5905  imadisj  5942  idrefALT  5967  intirr  5972  resco  6097  funcnv3  6418  fncnv  6421  fun11  6422  fununi  6423  mptfnf  6477  f1mpt  7010  mpomptx  7254  uniuni  7472  frxp  7811  oeeu  8219  ixp0x  8479  xpcomco  8596  1sdom  8710  dffi3  8884  wemapsolem  9003  cardval3  9370  kmlem4  9568  kmlem12  9576  kmlem14  9578  kmlem15  9579  kmlem16  9580  fpwwe2  10054  axgroth4  10243  ltexprlem4  10450  bitsmod  15775  pythagtrip  16161  isstruct  16486  pgpfac1  19133  pgpfac  19137  isassa  20018  basdif0  21491  ntreq0  21615  tgcmp  21939  tx1cn  22147  rnelfmlem  22490  phtpcer  23528  iscvsp  23661  caucfil  23815  minveclem1  23956  ovoliunlem1  24032  mdegleb  24587  istrkg2ld  26174  numedglnl  26857  usgr2pth0  27474  adjbd1o  29790  nelbOLD  30160  nmo  30182  dmrab  30188  difrab2  30189  mpomptxf  30354  ccfldextdgrr  30957  isros  31327  1stmbfm  31418  bnj976  31949  bnj1143  31962  bnj1533  32024  bnj864  32094  bnj983  32123  bnj1174  32173  bnj1175  32174  bnj1280  32190  cvmlift2lem12  32459  axacprim  32831  dmscut  33170  dfrecs2  33309  andnand1  33647  bj-denotes  34086  bj-snglc  34179  bj-disj2r  34238  bj-dfmpoa  34303  bj-mpomptALT  34304  mptsnunlem  34502  wl-cases2-dnf  34635  wl-euae  34640  wl-dfralv  34723  itg2addnc  34828  asindmre  34859  brres2  35412  brxrn2  35509  dfxrn2  35510  inxpxrn  35525  refsymrel2  35685  refsymrel3  35686  dfeqvrel2  35707  dfeqvrel3  35708  isopos  36198  dihglblem6  38358  dihglb2  38360  fgraphopab  39690  ifpid2g  39739  ifpim23g  39741  rp-fakeanorass  39759  en2pr  39786  elmapintrab  39816  relnonrel  39827  undmrnresiss  39844  elintima  39878  relexp0eq  39926  iunrelexp0  39927  dffrege115  40204  frege131  40220  frege133  40222  ntrneikb  40324  onfrALTlem5  40756  onfrALTlem5VD  41099  ndisj2  41193  ndmaovcom  43285  eliunxp2  44280  mpomptx2  44281  alimp-no-surprise  44780  alsi-no-surprise  44795
  Copyright terms: Public domain W3C validator