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

Theorem bitr2i 264
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 263 . 2 (𝜑𝜒)
43bicomi 213 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  3bitrri  286  3bitr2ri  288  3bitr4ri  292  nan  602  pm4.15  603  pm5.17  928  pm4.83  966  pm5.7  971  3or6  1402  nanim  1444  19.12vvv  1894  19.12vv  2168  cvjust  2605  abbi  2724  necon1abii  2830  nabbi  2884  nrexralim  2982  r19.23v  3005  ralnex2  3027  ralnex3  3028  spc3gv  3271  ralxpxfr2d  3298  sbc8g  3410  ss2rab  3641  difdif  3698  ddif  3704  unass  3732  unss  3749  undi  3833  rabeq0OLD  3914  disj  3969  ssindif0  3983  prneimg  4328  pwsnALT  4367  rabasiun  4459  iinrab2  4519  unopab  4660  axrep5  4704  eqvinop  4881  pwssun  4944  dmun  5253  reldm0  5264  dmres  5339  imadmrn  5395  ssrnres  5491  dmsnn0  5518  coundi  5553  coundir  5554  cnvpo  5590  xpco  5592  fun11  5877  fununi  5878  isarep1  5891  fdmrn  5977  dffv2  6181  fsn  6308  eufnfv  6395  eloprabga  6645  funoprabg  6657  ralrnmpt2  6673  pwexb  6867  suceloni  6905  funcnvuni  7012  oprabrexex2  7049  fsplit  7169  dfer2  7630  euen1b  7913  xpsnen  7929  1sdom  8048  wemapsolem  8338  zfregcl  8382  zfregclOLD  8384  epfrs  8490  rankbnd  8614  rankbnd2  8615  rankxplim2  8626  rankxplim3  8627  isinfcard  8798  dfac5lem2  8830  dfac5lem5  8833  kmlem14  8868  kmlem15  8869  kmlem16  8870  axdc2lem  9153  axcclem  9162  ac9  9188  ac9s  9198  nnunb  11165  xrrebnd  11873  elfznelfzo  12439  hashfun  13084  hashtpg  13121  rexuz3  13936  imasaddfnlem  16011  isnsgrp  17111  dprd2d2  18266  isnirred  18523  subsubrg2  18630  isdomn2  19120  mdetunilem8  20244  maducoeval2  20265  tgval2  20571  0top  20598  ssntr  20672  uncmp  21016  opnfbas  21456  fbunfip  21483  hausflf2  21612  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALT  21665  metrest  22139  cfilucfil3  22925  ellimc3  23449  plyun0  23757  sinhalfpilem  24019  2lgslem4  24931  dfcgra2  25521  colinearalg  25590  axcontlem5  25648  nb3graprlem2  25981  2wlkeq  26235  clwwlkn2  26303  clwlkisclwwlklem2a4  26312  el2wlkonot  26396  el2spthonot  26397  shlesb1i  27629  pjneli  27966  cnlnssadj  28323  pjin2i  28436  cvnbtwn2  28530  cvnbtwn4  28532  mdsl1i  28564  mdsl2i  28565  hatomistici  28605  cdj3lem3b  28683  iuninc  28761  disjex  28787  disjexc  28788  fpwrelmapffslem  28895  fpwrelmapffs  28897  isarchi2  29070  ismntop  29398  coinfliprv  29871  ballotlem2  29877  ballotlemi1  29891  plymulx  29951  bnj168  30052  bnj153  30204  bnj605  30231  bnj607  30240  bnj986  30278  bnj1090  30301  bnj1128  30312  dfso2  30897  dfpo2  30898  19.12b  30951  soseq  30995  dfom5b  31189  elfuns  31192  dfint3  31229  hfext  31460  trer  31480  bj-abbi  31963  bj-axrep5  31980  wl-nannot  32478  cnambfre  32628  itg2addnclem2  32632  itg2addnc  32634  heiborlem1  32780  lssat  33321  islshpat  33322  lcvnbtwn2  33332  pclfinclN  34254  lhpex2leN  34317  diclspsn  35501  dihmeetlem4preN  35613  dihmeetlem13N  35626  lcdlss  35926  mapd1o  35955  eq0rabdioph  36358  rmspecnonsq  36490  rmxdioph  36601  wopprc  36615  islssfg2  36659  ifpan23  36823  ifpid1g  36858  dfrtrcl5  36955  dfhe3  37089  ntrneikb  37412  ntrneixb  37413  2sbc6g  37638  2sbc5g  37639  iotasbc2  37643  2sb5nd  37797  2sb5ndVD  38168  2sb5ndALT  38190  2rexsb  39819  2rexrsb  39820  nb3grprlem2  40609  1wlkeq  40838  isspthonpth-av  40955  clwlkclwwlklem2a4  41206  clwwlksn2  41217  iseupthf1o  41369  fusgreg2wsp  41500  islindeps  42036
  Copyright terms: Public domain W3C validator