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

Theorem bitr2i 263
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
bitr2i.1 (𝜑𝜓)
bitr2i.2 (𝜓𝜒)
Assertion
Ref Expression
bitr2i (𝜒𝜑)

Proof of Theorem bitr2i
StepHypRef Expression
1 bitr2i.1 . . 3 (𝜑𝜓)
2 bitr2i.2 . . 3 (𝜓𝜒)
31, 2bitri 262 . 2 (𝜑𝜒)
43bicomi 212 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  3bitrri  285  3bitr2ri  287  3bitr4ri  291  nan  601  pm4.15  602  pm5.17  927  pm4.83  965  pm5.7  970  3or6  1401  nanim  1443  19.12vvv  1893  19.12vv  2163  cvjust  2601  abbi  2720  necon1abii  2826  nabbi  2880  nrexralim  2978  r19.23v  3001  ralnex2  3023  ralnex3  3024  spc3gv  3267  ralxpxfr2d  3294  sbc8g  3406  ss2rab  3637  difdif  3694  ddif  3700  unass  3728  unss  3745  undi  3829  rabeq0OLD  3910  disj  3965  ssindif0  3979  prneimg  4320  pwsnALT  4358  rabasiun  4450  iinrab2  4510  unopab  4651  axrep5  4695  eqvinop  4872  pwssun  4931  dmun  5237  reldm0  5248  dmres  5323  imadmrn  5379  ssrnres  5474  dmsnn0  5501  coundi  5536  coundir  5537  cnvpo  5573  xpco  5575  fun11  5860  fununi  5861  isarep1  5874  fdmrn  5960  dffv2  6163  fsn  6290  eufnfv  6370  eloprabga  6620  funoprabg  6632  ralrnmpt2  6648  pwexb  6841  suceloni  6879  funcnvuni  6986  oprabrexex2  7023  fsplit  7143  dfer2  7604  euen1b  7887  xpsnen  7903  1sdom  8022  wemapsolem  8312  zfregcl  8356  zfregclOLD  8358  epfrs  8464  rankbnd  8588  rankbnd2  8589  rankxplim2  8600  rankxplim3  8601  isinfcard  8772  dfac5lem2  8804  dfac5lem5  8807  kmlem14  8842  kmlem15  8843  kmlem16  8844  axdc2lem  9127  axcclem  9136  ac9  9162  ac9s  9172  nnunb  11132  xrrebnd  11829  elfznelfzo  12391  hashfun  13033  hashtpg  13068  rexuz3  13879  imasaddfnlem  15954  isnsgrp  17054  dprd2d2  18209  isnirred  18466  subsubrg2  18573  isdomn2  19063  mdetunilem8  20183  maducoeval2  20204  tgval2  20510  0top  20537  ssntr  20611  uncmp  20955  opnfbas  21395  fbunfip  21422  hausflf2  21551  alexsubALTlem2  21601  alexsubALTlem3  21602  alexsubALT  21604  metrest  22077  cfilucfil3  22839  ellimc3  23363  plyun0  23671  sinhalfpilem  23933  2lgslem4  24845  dfcgra2  25436  colinearalg  25505  axcontlem5  25563  nb3graprlem2  25744  2wlkeq  25998  clwwlkn2  26066  clwlkisclwwlklem2a4  26075  el2wlkonot  26159  el2spthonot  26160  shlesb1i  27432  pjneli  27769  cnlnssadj  28126  pjin2i  28239  cvnbtwn2  28333  cvnbtwn4  28335  mdsl1i  28367  mdsl2i  28368  hatomistici  28408  cdj3lem3b  28486  iuninc  28564  disjex  28590  disjexc  28591  fpwrelmapffslem  28698  fpwrelmapffs  28700  isarchi2  28873  ismntop  29201  coinfliprv  29674  ballotlem2  29680  ballotlemi1  29694  plymulx  29754  bnj168  29855  bnj153  30007  bnj605  30034  bnj607  30043  bnj986  30081  bnj1090  30104  bnj1128  30115  dfso2  30700  dfpo2  30701  19.12b  30754  soseq  30798  dfom5b  30992  elfuns  30995  dfint3  31032  hfext  31263  trer  31283  bj-abbi  31773  bj-axrep5  31790  wl-nannot  32278  cnambfre  32428  itg2addnclem2  32432  itg2addnc  32434  heiborlem1  32580  lssat  33121  islshpat  33122  lcvnbtwn2  33132  pclfinclN  34054  lhpex2leN  34117  diclspsn  35301  dihmeetlem4preN  35413  dihmeetlem13N  35426  lcdlss  35726  mapd1o  35755  eq0rabdioph  36158  rmspecnonsq  36290  rmxdioph  36401  wopprc  36415  islssfg2  36459  ifpan23  36623  ifpid1g  36658  dfrtrcl5  36755  dfhe3  36889  ntrneikb  37212  ntrneixb  37213  2sbc6g  37438  2sbc5g  37439  iotasbc2  37443  2sb5nd  37597  2sb5ndVD  37968  2sb5ndALT  37990  2rexsb  39620  2rexrsb  39621  nb3grprlem2  40608  1wlkeq  40837  isspthonpth-av  40954  clwlkclwwlklem2a4  41205  clwwlksn2  41216  iseupthf1o  41368  fusgreg2wsp  41499  islindeps  42035
  Copyright terms: Public domain W3C validator