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

Theorem bitr2i 275
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 274 . 2 (𝜑𝜒)
43bicomi 223 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:  3bitrri  297  3bitr2ri  299  3bitr4ri  303  nan  828  pm4.15  831  pm5.7  952  pm5.17  1010  pm4.83  1023  3or6  1447  nanim  1496  nannot  1497  empty  1909  19.12vvv  1992  19.12vv  2343  cvjust  2730  abbi  2808  necon1abii  2990  nabbi  3045  nrexralim  3132  r19.23v  3177  nelb  3220  spc3gv  3561  ralxpxfr2d  3594  sbc8g  3745  csbied  3891  ss2rab  4026  difdif  4088  ddif  4094  unass  4124  unss  4142  undi  4232  vn0  4296  ab0orv  4336  disj  4405  disjOLD  4406  ssindif0  4421  prneimg  4810  pwsnOLD  4856  iinrab2  5028  unopab  5185  axrep5  5246  eqvinop  5442  pwssun  5526  dmun  5864  reldm0  5881  dmres  5957  imadmrn  6021  ssrnres  6128  dmsnn0  6157  coundi  6197  coundir  6198  resco  6200  cnvpo  6237  xpco  6239  dfpo2  6246  fun11  6572  fununi  6573  isarep1OLD  6588  fdmrn  6697  dffv2  6933  fsn  7077  eufnfv  7175  eloprabga  7460  eloprabgaOLD  7461  funoprabg  7473  ralrnmpo  7490  imaeqexov  7588  sucexeloniOLD  7741  suceloniOLD  7743  tfinds2  7796  funcnvuni  7864  oprabrexex2  7907  ralxp3f  8065  soseq  8087  dfer2  8645  euen1b  8967  xpsnen  8995  1sdomOLD  9189  wemapsolem  9482  zfregcl  9526  epfrs  9663  rankbnd  9800  rankbnd2  9801  rankxplim2  9812  rankxplim3  9813  isinfcard  10024  dfac5lem2  10056  dfac5lem5  10059  kmlem14  10095  kmlem15  10096  kmlem16  10097  axdc2lem  10380  axcclem  10389  ac9  10415  ac9s  10425  nnunb  12405  xrrebnd  13079  elfznelfzo  13669  hashfun  14329  hashtpg  14376  rexuz3  15225  imasaddfnlem  17402  isnsgrp  18542  dprd2d2  19814  isnirred  20114  subsubrg2  20234  isdomn2  20754  mdetunilem8  21952  maducoeval2  21973  tgval2  22290  0top  22317  ssntr  22393  uncmp  22738  opnfbas  23177  fbunfip  23204  alexsubALTlem2  23383  alexsubALTlem3  23384  alexsubALT  23386  metrest  23864  cfilucfil3  24668  ellimc3  25227  plyun0  25542  sinhalfpilem  25804  2lgslem4  26738  dfcgra2  27658  colinearalg  27745  axcontlem5  27803  nb3grprlem2  28215  wlkeq  28468  isspthonpth  28583  clwlkclwwlklem2a4  28827  clwwlkn1  28871  clwwlkn2  28874  clwwlknon2x  28933  fusgreg2wsp  29166  h2hlm  29808  shlesb1i  30214  pjneli  30551  cnlnssadj  30908  pjin2i  31021  cvnbtwn2  31115  cvnbtwn4  31117  mdsl1i  31149  mdsl2i  31150  hatomistici  31190  cdj3lem3b  31268  iuninc  31365  disjex  31396  disjexc  31397  fpwrelmapffslem  31532  fpwrelmapffs  31534  mgcval  31730  isarchi2  31904  ismntop  32476  coinfliprv  32951  ballotlem2  32957  ballotlemi1  32971  plymulx  33029  oddprm2  33137  bnj168  33211  bnj153  33361  bnj605  33388  bnj607  33397  bnj986  33436  bnj1090  33460  bnj1128  33471  fineqvrep  33565  fmlasucdisj  33862  dfso2  34198  19.12b  34246  dfom5b  34464  elfuns  34467  dfint3  34504  hfext  34735  trer  34755  bj-alcomexcom  35112  wl-3xornot1  35918  wl-df3maxtru1  35930  cnambfre  36093  itg2addnclem2  36097  itg2addnc  36099  heiborlem1  36237  inxpxrn  36824  lssat  37445  islshpat  37446  lcvnbtwn2  37456  pclfinclN  38380  lhpex2leN  38443  diclspsn  39624  dihmeetlem4preN  39736  dihmeetlem13N  39749  lcdlss  40049  mapd1o  40078  eq0rabdioph  41037  rmspecnonsq  41168  rmxdioph  41278  wopprc  41292  islssfg2  41336  ifpan23  41674  ifpid1g  41708  minregex  41748  dfrtrcl5  41843  dfhe3  41989  ntrneikb  42308  scottabf  42462  2sbc6g  42637  2sbc5g  42638  iotasbc2  42642  2sb5nd  42784  2sb5ndVD  43134  2sb5ndALT  43156  limsupre2lem  43897  2rexsb  45265  2rexrsb  45266  islindeps  46466  io1ii  46885
  Copyright terms: Public domain W3C validator