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  1507  sbrimvlem  2094  dfsb7OLD  2280  2eu4  2739  2eu5  2740  2eu5OLD  2741  euxfrw  3715  euxfr  3717  euind  3718  rmo4  3724  rmo3f  3728  2reu5lem3  3751  rmo3  3875  rmo3OLD  3876  difin  4241  axsepgfromrep  5197  reusv2lem4  5297  rabxp  5598  elvvv  5625  eliunxp  5706  elidinxp  5909  imadisj  5945  idrefALT  5970  intirr  5975  resco  6100  funcnv3  6420  fncnv  6423  fun11  6424  fununi  6425  mptfnf  6479  f1mpt  7016  mpomptx  7258  uniuni  7476  frxp  7814  oeeu  8222  ixp0x  8482  xpcomco  8599  1sdom  8713  dffi3  8887  wemapsolem  9006  cardval3  9373  kmlem4  9571  kmlem12  9579  kmlem14  9581  kmlem15  9582  kmlem16  9583  fpwwe2  10057  axgroth4  10246  ltexprlem4  10453  bitsmod  15777  pythagtrip  16163  isstruct  16488  pgpfac1  19124  pgpfac  19128  isassa  20009  basdif0  21477  ntreq0  21601  tgcmp  21925  tx1cn  22133  rnelfmlem  22476  phtpcer  23514  iscvsp  23647  caucfil  23801  minveclem1  23942  ovoliunlem1  24018  mdegleb  24573  istrkg2ld  26160  numedglnl  26843  usgr2pth0  27460  adjbd1o  29776  nelbOLD  30146  nmo  30168  dmrab  30174  difrab2  30175  mpomptxf  30340  ccfldextdgrr  30943  isros  31313  1stmbfm  31404  bnj976  31935  bnj1143  31948  bnj1533  32010  bnj864  32080  bnj983  32109  bnj1174  32159  bnj1175  32160  bnj1280  32176  cvmlift2lem12  32445  axacprim  32817  dmscut  33156  dfrecs2  33295  andnand1  33633  bj-denotes  34072  bj-snglc  34165  bj-disj2r  34224  bj-dfmpoa  34289  bj-mpomptALT  34290  mptsnunlem  34488  wl-cases2-dnf  34621  wl-euae  34626  wl-dfralv  34708  itg2addnc  34813  asindmre  34844  brres2  35397  brxrn2  35494  dfxrn2  35495  inxpxrn  35510  refsymrel2  35670  refsymrel3  35671  dfeqvrel2  35692  dfeqvrel3  35693  isopos  36183  dihglblem6  38343  dihglb2  38345  fgraphopab  39671  ifpid2g  39720  ifpim23g  39722  rp-fakeanorass  39740  en2pr  39767  elmapintrab  39797  relnonrel  39808  undmrnresiss  39825  elintima  39859  relexp0eq  39907  iunrelexp0  39908  dffrege115  40185  frege131  40201  frege133  40203  ntrneikb  40305  onfrALTlem5  40737  onfrALTlem5VD  41080  ndisj2  41174  ndmaovcom  43266  eliunxp2  44210  mpomptx2  44211  alimp-no-surprise  44710  alsi-no-surprise  44725
  Copyright terms: Public domain W3C validator