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

Theorem bitr2i 265
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 264 . 2 (𝜑𝜒)
43bicomi 214 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  3bitrri  287  3bitr2ri  289  3bitr4ri  293  nan  604  pm4.15  605  pm5.17  932  pm4.83  970  pm5.7  975  3or6  1409  nanim  1451  19.12vvv  1906  19.12vv  2179  cvjust  2616  abbi  2736  necon1abii  2841  nabbi  2895  nrexralim  2998  r19.23v  3021  ralnex2  3043  ralnex3  3044  spc3gv  3296  ralxpxfr2d  3325  sbc8g  3441  ss2rab  3676  difdif  3734  ddif  3740  unass  3768  unss  3785  undi  3872  rabeq0OLD  3958  disj  4015  ssindif0  4029  prneimg  4386  pwsnALT  4427  iinrab2  4581  unopab  4726  axrep5  4774  eqvinop  4953  pwssun  5018  dmun  5329  reldm0  5341  dmres  5417  imadmrn  5474  ssrnres  5570  dmsnn0  5598  coundi  5634  coundir  5635  cnvpo  5671  xpco  5673  fun11  5961  fununi  5962  isarep1  5975  fdmrn  6062  dffv2  6269  fsn  6399  eufnfv  6488  eloprabga  6744  funoprabg  6756  ralrnmpt2  6772  suceloni  7010  funcnvuni  7116  oprabrexex2  7155  fsplit  7279  dfer2  7740  euen1b  8024  xpsnen  8041  1sdom  8160  wemapsolem  8452  zfregcl  8496  zfregclOLD  8498  epfrs  8604  rankbnd  8728  rankbnd2  8729  rankxplim2  8740  rankxplim3  8741  isinfcard  8912  dfac5lem2  8944  dfac5lem5  8947  kmlem14  8982  kmlem15  8983  kmlem16  8984  axdc2lem  9267  axcclem  9276  ac9  9302  ac9s  9312  nnunb  11285  xrrebnd  11996  elfznelfzo  12569  hashfun  13219  hashtpg  13262  rexuz3  14082  imasaddfnlem  16182  isnsgrp  17282  dprd2d2  18437  isnirred  18694  subsubrg2  18801  isdomn2  19293  mdetunilem8  20419  maducoeval2  20440  tgval2  20754  0top  20781  ssntr  20856  uncmp  21200  opnfbas  21640  fbunfip  21667  hausflf2  21796  alexsubALTlem2  21846  alexsubALTlem3  21847  alexsubALT  21849  metrest  22323  cfilucfil3  23111  ellimc3  23637  plyun0  23947  sinhalfpilem  24209  2lgslem4  25125  dfcgra2  25715  colinearalg  25784  axcontlem5  25842  nb3grprlem2  26277  wlkeq  26523  isspthonpth  26639  clwlkclwwlklem2a4  26892  clwwlksn2  26903  fusgreg2wsp  27187  shlesb1i  28229  pjneli  28566  cnlnssadj  28923  pjin2i  29036  cvnbtwn2  29130  cvnbtwn4  29132  mdsl1i  29164  mdsl2i  29165  hatomistici  29205  cdj3lem3b  29283  iuninc  29363  disjex  29389  disjexc  29390  fpwrelmapffslem  29492  fpwrelmapffs  29494  isarchi2  29724  ismntop  30055  coinfliprv  30529  ballotlem2  30535  ballotlemi1  30549  plymulx  30610  oddprm2  30718  bnj168  30783  bnj153  30935  bnj605  30962  bnj607  30971  bnj986  31009  bnj1090  31032  bnj1128  31043  dfso2  31630  dfpo2  31631  19.12b  31691  soseq  31735  dfom5b  32003  elfuns  32006  dfint3  32043  hfext  32274  trer  32294  bj-abbi  32759  bj-axrep5  32776  wl-nannot  33279  cnambfre  33438  itg2addnclem2  33442  itg2addnc  33444  heiborlem1  33590  lssat  34129  islshpat  34130  lcvnbtwn2  34140  pclfinclN  35062  lhpex2leN  35125  diclspsn  36309  dihmeetlem4preN  36421  dihmeetlem13N  36434  lcdlss  36734  mapd1o  36763  eq0rabdioph  37166  rmspecnonsq  37298  rmxdioph  37409  wopprc  37423  islssfg2  37467  ifpan23  37630  ifpid1g  37665  dfrtrcl5  37762  dfhe3  37895  ntrneikb  38218  ntrneixb  38219  2sbc6g  38442  2sbc5g  38443  iotasbc2  38447  2sb5nd  38602  2sb5ndVD  38972  2sb5ndALT  38994  limsupre2lem  39762  2rexsb  40939  2rexrsb  40940  islindeps  42013
  Copyright terms: Public domain W3C validator