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

Theorem bitr2i 277
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 276 . 2 (𝜑𝜒)
43bicomi 225 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:  3bitrri  299  3bitr2ri  301  3bitr4ri  305  nan  827  pm4.15  830  pm5.7  949  pm5.17  1007  pm4.83  1020  3or6  1440  nanim  1484  nannot  1485  empty  1900  19.12vvv  1988  19.12vv  2362  cvjust  2821  abbi  2893  abbiOLD  2960  necon1abii  3069  nabbi  3126  ralnex2OLD  3266  ralnex3OLD  3268  nrexralim  3271  r19.23v  3284  spc3gv  3609  ralxpxfr2d  3643  sbc8g  3784  ss2rab  4051  difdif  4111  ddif  4117  unass  4146  unss  4164  undi  4255  disj  4402  ssindif0  4416  prneimg  4784  pwsnALT  4830  iinrab2  4989  unopab  5142  axrep5  5193  eqvinop  5375  pwssun  5454  dmun  5778  reldm0  5797  dmres  5874  imadmrn  5938  ssrnres  6034  dmsnn0  6063  coundi  6099  coundir  6100  resco  6102  cnvpo  6137  xpco  6139  fun11  6427  fununi  6428  isarep1  6441  fdmrn  6537  dffv2  6755  fsn  6895  eufnfv  6988  eloprabga  7255  funoprabg  7267  ralrnmpo  7283  suceloni  7521  tfinds2  7571  funcnvuni  7629  oprabrexex2  7675  fsplitOLD  7809  dfer2  8285  euen1b  8574  xpsnen  8595  1sdom  8715  wemapsolem  9008  zfregcl  9052  epfrs  9167  rankbnd  9291  rankbnd2  9292  rankxplim2  9303  rankxplim3  9304  isinfcard  9512  dfac5lem2  9544  dfac5lem5  9547  kmlem14  9583  kmlem15  9584  kmlem16  9585  axdc2lem  9864  axcclem  9873  ac9  9899  ac9s  9909  nnunb  11887  xrrebnd  12556  elfznelfzo  13137  hashfun  13793  hashtpg  13838  rexuz3  14703  imasaddfnlem  16796  isnsgrp  17900  dprd2d2  19102  isnirred  19386  subsubrg2  19498  isdomn2  20007  mdetunilem8  21163  maducoeval2  21184  tgval2  21499  0top  21526  ssntr  21601  uncmp  21946  opnfbas  22385  fbunfip  22412  alexsubALTlem2  22591  alexsubALTlem3  22592  alexsubALT  22594  metrest  23068  cfilucfil3  23857  ellimc3  24411  plyun0  24721  sinhalfpilem  24983  2lgslem4  25915  dfcgra2  26549  colinearalg  26629  axcontlem5  26687  nb3grprlem2  27096  wlkeq  27348  isspthonpth  27463  clwlkclwwlklem2a4  27708  clwwlkn1  27752  clwwlkn2  27755  clwwlknon2x  27815  fusgreg2wsp  28048  h2hlm  28690  shlesb1i  29096  pjneli  29433  cnlnssadj  29790  pjin2i  29903  cvnbtwn2  29997  cvnbtwn4  29999  mdsl1i  30031  mdsl2i  30032  hatomistici  30072  cdj3lem3b  30150  nelbOLD  30165  iuninc  30246  disjex  30276  disjexc  30277  fpwrelmapffslem  30400  fpwrelmapffs  30402  isarchi2  30747  ismntop  31172  coinfliprv  31645  ballotlem2  31651  ballotlemi1  31665  plymulx  31723  oddprm2  31831  bnj168  31905  bnj153  32057  bnj605  32084  bnj607  32093  bnj986  32131  bnj1090  32154  bnj1128  32165  fmlasucdisj  32549  dfso2  32893  dfpo2  32894  19.12b  32949  soseq  32999  dfom5b  33276  elfuns  33279  dfint3  33316  hfext  33547  trer  33567  cnambfre  34826  itg2addnclem2  34830  itg2addnc  34832  heiborlem1  34976  inxpxrn  35529  lssat  36038  islshpat  36039  lcvnbtwn2  36049  pclfinclN  36972  lhpex2leN  37035  diclspsn  38216  dihmeetlem4preN  38328  dihmeetlem13N  38341  lcdlss  38641  mapd1o  38670  eq0rabdioph  39257  rmspecnonsq  39388  rmxdioph  39497  wopprc  39511  islssfg2  39555  ifpan23  39709  ifpid1g  39744  dfrtrcl5  39873  dfhe3  40005  ntrneikb  40328  scottabf  40460  2sbc6g  40631  2sbc5g  40632  iotasbc2  40636  2sb5nd  40778  2sb5ndVD  41128  2sb5ndALT  41150  limsupre2lem  41889  2rexsb  43184  2rexrsb  43185  islindeps  44410
  Copyright terms: Public domain W3C validator