MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr3i Unicode version

Theorem bitr3i 244
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3i.1
bitr3i.2
Assertion
Ref Expression
bitr3i

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3
21bicomi 195 . 2
3 bitr3i.2 . 2
42, 3bitri 242 1
Colors of variables: wff set class
Syntax hints:  <->wb 178
This theorem is referenced by:  3bitrri  265  3bitr3i  268  3bitr3ri  269  xchnxbi  301  ianor  476  orordi  518  orordir  519  anandi  803  anandir  804  trunantru  1372  falnanfal  1375  cadanOLD  1411  had0  1422  nic-axALT  1458  sbied  2152  sb6a  2207  sbelx  2220  sbco4  2230  mo  2337  2eu6  2411  abeq1i  2589  necon1bbii  2701  r19.41  2906  2ralor  2924  rexcom4a  3026  moeq  3161  2reuswap  3187  2reu5  3193  nfcdeq  3209  sbcid  3228  sbcco2  3235  sbc7  3239  sbcie2g  3245  eqsbc3  3251  sbcralt  3292  cbvralcsf  3344  cbvrabcsf  3347  abss  3445  ssab  3446  difrab  3647  neq0  3670  sbccsb  3723  vdif0  3760  difrab0eq  3761  ssunsn2  4043  sspr  4047  sstp  4048  prsspw  4056  uniintsn  4175  disjmoOLD  4287  brab1  4347  unopab  4377  axrep5  4418  axsep  4422  intexab  4457  reusv2lem4  4503  reusv2  4505  reuxfrd  4524  wefrc  4717  ordelord  4744  elvvv  4902  eliunxp  4981  ralxp  4985  rexxp  4986  opelco  5015  reldm0  5061  resieq  5125  iss  5157  imai  5183  cnvsym  5214  intasym  5215  asymref  5216  codir  5220  poirr2  5224  rninxp  5277  dffun3  5428  funopg  5449  fin  5587  f1cnvcnv  5608  funimass4  5735  fnressn  5880  resoprab  6155  mpt22eqb  6168  ov6g  6196  offval  6294  uniuni  6350  dfwe2  6358  orduniorsuc  6406  tfinds2  6439  resiexg  6479  dfopab2  6589  dfoprab3s  6590  fmpt2x  6601  fparlem1  6629  fparlem2  6630  brtpos0  6669  dftpos3  6680  tpostpos  6682  tz7.48lem  6810  omeu  6940  ercnv  7038  ixp0  7207  xpcomco  7310  xpassen  7314  php  7403  findcard3  7462  ixpfi2  7517  dfsup2  7559  card2on  7634  infeq5i  7703  cnfcom3lem  7772  r1elss  7844  rankxplim  7917  scott0s  7926  aceq1  8112  dfac5lem1  8118  dfac5lem2  8119  kmlem3  8146  kmlem8  8151  kmlem16  8159  cflem  8240  cf0  8245  alephval2  8561  rankcf  8766  r1tskina  8771  wfgru  8805  genpass  9000  psslinpr  9022  ltpsrpr  9098  infm3  10098  nnwos  10729  ioo0  11132  ico0  11153  ioc0  11154  icc0  11155  elfz2nn0  11279  elfzmlbp  11290  sqeqori  11770  hashgt12el  11965  hashgt12el2  11966  cshwidxmod  12226  clim0  12770  dvdslelem  13363  divalglem6  13388  isprm2lem  13556  pceu  13699  prmreclem2  13764  cshwshash  13917  isstruct  13970  xpscf  14282  acsfn2  14379  invsym2  14479  pospo  14921  efgrelexlemb  15885  gexex  15971  lssne0  16530  opsrtoslem1  17047  opsrtoslem2  17048  ntreq0  17644  ordtrest2lem  17770  ist0-3  17912  ist1-2  17914  ist1-3  17916  cmpfi  17974  2ndcctbss  18022  ptbasfi  18117  ptcnplem  18157  hausdiag  18181  hauseqlcld  18182  cnmptcom  18214  txflf  18542  tgphaus  18650  metrest  19058  iccpnfcnv  19473  bcth3  19788  volun  19943  dyadmax  19994  vitalilem2  20005  vitalilem3  20006  mbfimaopnlem  20049  itg2leub  20128  dvres2  20303  ellogdm  21039  reasinsin  21245  leibpilem2  21290  ftalem3  21366  dchreq  21551  lnon0  22808  spansncvi  23665  pjssmii  23694  nmlnopgt0i  24011  largei  24281  cvexchlem  24382  xfree  24458  nmo  24485  2reuswap2  24488  fpwrelmapffslem  24653  addeq0  24656  eliccioo  24727  omndmul2  24798  ordtrest2NEWlem  25022  ordtconlem1  25024  xrge0iifcnv  25033  xrge0iifiso  25035  xrge0iifhom  25037  cntnevol  25313  eulerpartlemgh  25426  ballotlemfp1  25515  ballotlem7  25559  signswch  25604  derang0  25694  iccllyscon  25776  cvmsss2  25800  axacprim  25989  dftr6  26203  dfpo2  26208  opelco3  26233  elima4  26234  setinds2f  26236  elpotr  26238  tz6.26  26310  wfis2fg  26316  frins2fg  26352  wzel  26405  nobndlem1  26477  elfuns  26590  dfiota3  26598  imagesset  26628  axcontlem2  26734  lineunray  26911  ellines  26916  hfninf  26957  tan2h  27096  ovoliunnfl  27104  voliunnfl  27106  ftc1anc  27146  inixp  27293  heibor1lem  27381  tsna1  27589  4rexfrabdioph  27787  dford4  28029  islindf4  28214  f1omvdco3  28298  psgnunilem5  28323  isdomn3  28429  fgraphopab  28435  2rmoswap  28862  ndmaovcom  28967  rabasiun  29089  wlk0  29151  usgra2pth0  29161  rusgranumwlklem0  29425  frgra3v  29453  4cycl2vnunb  29468  vdn0frgrav2  29475  vdgn0frgrav2  29476  usg2spot2nb  29517  opelopab4  29829  2sb5nd  29838  un2122  30093  uunT12p4  30106  onfrALTlem5VD  30190  2sb5ndVD  30215  2sb5ndALT  30237  bnj446  30274  bnj563  30304  bnj110  30422  bnj153  30444  bnj557  30465  bnj864  30486  bnj865  30487  bnj849  30489  bnj929  30500  bnj1110  30544  bj-snglc  30675  sbelxNEW11  30887  ax11w14lemAUX11  30943  islshpat  31088  lkr0f  31165  lshpsmreu  31180  cvrnbtwn4  31350  ishlat2  31424  islvol5  31649  tendoeq2  32844  dibelval3  33218  mapdpglem3  33746  hdmapglem7a  34001
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 179
  Copyright terms: Public domain W3C validator