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

Theorem bitr2i 267
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 266 . 2 (𝜑𝜒)
43bicomi 215 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  3bitrri  289  3bitr2ri  291  3bitr4ri  295  nan  850  pm4.15  852  pm5.7  967  pm5.17  1026  pm4.83  1039  3or6  1564  nanim  1606  19.12vvv  2087  19.12vv  2356  cvjust  2812  abbi  2932  necon1abii  3037  nabbi  3091  nrexralim  3197  r19.23v  3222  ralnex2  3244  ralnex3  3245  spc3gv  3502  ralxpxfr2d  3532  sbc8g  3652  ss2rab  3886  difdif  3946  ddif  3952  unass  3980  unss  3997  undi  4087  disj  4225  ssindif0  4239  prneimg  4586  pwsnALT  4634  iinrab2  4786  unopab  4933  axrep5  4983  eqvinop  5157  pwssun  5228  dmun  5546  reldm0  5558  dmres  5636  imadmrn  5700  ssrnres  5797  dmsnn0  5825  coundi  5864  coundir  5865  cnvpo  5901  xpco  5903  fun11  6184  fununi  6185  isarep1  6198  fdmrn  6289  dffv2  6502  fsn  6635  eufnfv  6726  eloprabga  6987  funoprabg  6999  ralrnmpt2  7015  suceloni  7253  funcnvuni  7359  oprabrexex2  7398  fsplit  7526  dfer2  7990  euen1b  8273  xpsnen  8293  1sdom  8412  wemapsolem  8704  zfregcl  8748  epfrs  8864  rankbnd  8988  rankbnd2  8989  rankxplim2  9000  rankxplim3  9001  isinfcard  9208  dfac5lem2  9240  dfac5lem5  9243  kmlem14  9280  kmlem15  9281  kmlem16  9282  axdc2lem  9565  axcclem  9574  ac9  9600  ac9s  9610  nnunb  11575  xrrebnd  12237  elfznelfzo  12817  hashfun  13461  hashtpg  13504  rexuz3  14331  imasaddfnlem  16413  isnsgrp  17513  dprd2d2  18665  isnirred  18922  subsubrg2  19031  isdomn2  19528  mdetunilem8  20657  maducoeval2  20678  tgval2  20995  0top  21022  ssntr  21097  uncmp  21441  opnfbas  21880  fbunfip  21907  hausflf2  22036  alexsubALTlem2  22086  alexsubALTlem3  22087  alexsubALT  22089  metrest  22563  cfilucfil3  23351  ellimc3  23880  plyun0  24190  sinhalfpilem  24453  2lgslem4  25368  dfcgra2  25958  colinearalg  26027  axcontlem5  26085  nb3grprlem2  26522  wlkeq  26780  isspthonpth  26896  clwlkclwwlklem2a4  27163  clwwlkn1  27213  clwwlkn2  27216  clwwlknon2x  27294  fusgreg2wsp  27534  shlesb1i  28596  pjneli  28933  cnlnssadj  29290  pjin2i  29403  cvnbtwn2  29497  cvnbtwn4  29499  mdsl1i  29531  mdsl2i  29532  hatomistici  29572  cdj3lem3b  29650  iuninc  29727  disjex  29753  disjexc  29754  fpwrelmapffslem  29857  fpwrelmapffs  29859  isarchi2  30087  ismntop  30418  coinfliprv  30892  ballotlem2  30898  ballotlemi1  30912  plymulx  30973  oddprm2  31081  bnj168  31144  bnj153  31295  bnj605  31322  bnj607  31331  bnj986  31369  bnj1090  31392  bnj1128  31403  dfso2  31988  dfpo2  31989  19.12b  32049  soseq  32097  dfom5b  32362  elfuns  32365  dfint3  32402  hfext  32633  trer  32653  bj-abbi  33108  bj-axrep5  33125  wl-nannot  33634  cnambfre  33789  itg2addnclem2  33793  itg2addnc  33795  heiborlem1  33940  inxpxrn  34485  lssat  34815  islshpat  34816  lcvnbtwn2  34826  pclfinclN  35749  lhpex2leN  35812  diclspsn  36993  dihmeetlem4preN  37105  dihmeetlem13N  37118  lcdlss  37418  mapd1o  37447  eq0rabdioph  37860  rmspecnonsq  37991  rmxdioph  38102  wopprc  38116  islssfg2  38160  ifpan23  38322  ifpid1g  38357  dfrtrcl5  38454  dfhe3  38587  ntrneikb  38910  ntrneixb  38911  2sbc6g  39133  2sbc5g  39134  iotasbc2  39138  2sb5nd  39292  2sb5ndVD  39658  2sb5ndALT  39680  limsupre2lem  40454  2rexsb  41701  2rexrsb  41702  islindeps  42828
  Copyright terms: Public domain W3C validator