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

Theorem 3bitr2i 298
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 277 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 274 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  353  xorneg2  1520  sbrimvw  2094  2eu4  2655  2eu5  2656  euxfrw  3677  euxfr  3679  euind  3680  rmo4  3686  rmo3f  3690  2reu5lem3  3713  rmo3  3843  difin  4219  indifdi  4241  ab0orv  4336  dftr5  5224  axsepgfromrep  5252  reusv2lem4  5354  rabxp  5676  elvvv  5703  eliunxp  5789  elidinxp  5993  imadisj  6028  idrefALT  6061  intirr  6068  resco  6198  funcnv3  6566  fncnv  6569  fun11  6570  fununi  6571  mptfnf  6631  f1mpt  7202  mpomptx  7461  uniuni  7686  frxp  8046  oeeu  8517  ixp0x  8797  xpcomco  8939  1sdomOLD  9126  dffi3  9300  wemapsolem  9419  cardval3  9821  kmlem4  10022  kmlem12  10030  kmlem14  10032  kmlem15  10033  kmlem16  10034  fpwwe2  10512  axgroth4  10701  ltexprlem4  10908  bitsmod  16250  pythagtrip  16640  isstruct  16958  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  27200  numedglnl  27893  usgr2pth0  28511  adjbd1o  30825  nmo  31216  dmrab  31222  difrab2  31223  mpomptxf  31392  ccfldextdgrr  32139  isros  32540  1stmbfm  32633  bnj976  33162  bnj1143  33175  bnj1533  33237  bnj864  33307  bnj983  33336  bnj1174  33388  bnj1175  33389  bnj1280  33405  cvmlift2lem12  33681  axacprim  34053  xpord2pred  34180  xpord2ind  34182  dfrecs2  34430  andnand1  34768  bj-snglc  35335  bj-disj2r  35394  bj-dfmpoa  35484  bj-mpomptALT  35485  mptsnunlem  35704  wl-df3xor2  35835  wl-df4-3mintru2  35853  wl-cases2-dnf  35866  wl-euae  35871  itg2addnc  36027  asindmre  36056  brres2  36623  brxrn2  36732  dfxrn2  36733  inxpxrn  36752  refsymrel2  36924  refsymrel3  36925  dfeqvrel2  36947  dfeqvrel3  36948  isopos  37537  dihglblem6  39698  dihglb2  39700  fgraphopab  41402  dflim5  41420  ifpid2g  41527  ifpim23g  41529  rp-fakeanorass  41547  en2pr  41581  elmapintrab  41610  relnonrel  41621  undmrnresiss  41638  elintima  41687  relexp0eq  41735  iunrelexp0  41736  dffrege115  42012  frege131  42028  frege133  42030  ntrneikb  42130  onfrALTlem5  42588  onfrALTlem5VD  42931  ndisj2  43023  ndmaovcom  45186  eliunxp2  46158  mpomptx2  46159  mo0sn  46649  i0oii  46701  io1ii  46702  alimp-no-surprise  46973  alsi-no-surprise  46988
  Copyright terms: Public domain W3C validator