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

Theorem 3bitr2i 299
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 278 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 275 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 205
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 206
This theorem is referenced by:  con2bi  354  xorneg2  1521  sbrimvw  2095  2eu4  2656  2eu5  2657  euxfrw  3678  euxfr  3680  euind  3681  rmo4  3687  rmo3f  3691  2reu5lem3  3714  rmo3  3844  difin  4220  indifdi  4242  ab0orv  4337  dftr5  5225  axsepgfromrep  5253  reusv2lem4  5355  rabxp  5677  elvvv  5704  eliunxp  5790  elidinxp  5994  imadisj  6029  idrefALT  6062  intirr  6069  resco  6199  funcnv3  6567  fncnv  6570  fun11  6571  fununi  6572  mptfnf  6632  f1mpt  7203  mpomptx  7462  uniuni  7687  frxp  8047  oeeu  8518  ixp0x  8798  xpcomco  8940  1sdomOLD  9127  dffi3  9301  wemapsolem  9420  cardval3  9822  kmlem4  10023  kmlem12  10031  kmlem14  10033  kmlem15  10034  kmlem16  10035  fpwwe2  10513  axgroth4  10702  ltexprlem4  10909  bitsmod  16251  pythagtrip  16641  isstruct  16959  pgpfac1  19788  pgpfac  19792  isassa  21185  basdif0  22225  ntreq0  22350  tgcmp  22674  tx1cn  22882  rnelfmlem  23225  phtpcer  24280  iscvsp  24413  caucfil  24569  minveclem1  24710  ovoliunlem1  24788  mdegleb  25351  eqscut2  27067  dmscut  27072  made0  27124  istrkg2ld  27188  numedglnl  27881  usgr2pth0  28499  adjbd1o  30813  nmo  31204  dmrab  31210  difrab2  31211  mpomptxf  31380  ccfldextdgrr  32127  isros  32528  1stmbfm  32621  bnj976  33150  bnj1143  33163  bnj1533  33225  bnj864  33295  bnj983  33324  bnj1174  33376  bnj1175  33377  bnj1280  33393  cvmlift2lem12  33669  axacprim  34041  xpord2pred  34168  xpord2ind  34170  dfrecs2  34421  andnand1  34759  bj-snglc  35326  bj-disj2r  35385  bj-dfmpoa  35475  bj-mpomptALT  35476  mptsnunlem  35695  wl-df3xor2  35826  wl-df4-3mintru2  35844  wl-cases2-dnf  35857  wl-euae  35862  itg2addnc  36018  asindmre  36047  brres2  36614  brxrn2  36723  dfxrn2  36724  inxpxrn  36743  refsymrel2  36915  refsymrel3  36916  dfeqvrel2  36938  dfeqvrel3  36939  isopos  37528  dihglblem6  39689  dihglb2  39691  fgraphopab  41371  dflim5  41389  ifpid2g  41496  ifpim23g  41498  rp-fakeanorass  41516  en2pr  41550  elmapintrab  41579  relnonrel  41590  undmrnresiss  41607  elintima  41656  relexp0eq  41704  iunrelexp0  41705  dffrege115  41981  frege131  41997  frege133  41999  ntrneikb  42099  onfrALTlem5  42557  onfrALTlem5VD  42900  ndisj2  42992  ndmaovcom  45155  eliunxp2  46127  mpomptx2  46128  mo0sn  46618  i0oii  46670  io1ii  46671  alimp-no-surprise  46942  alsi-no-surprise  46957
  Copyright terms: Public domain W3C validator