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

Theorem bitr3i 266
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.)
Hypotheses
Ref Expression
bitr3i.1 (𝜓𝜑)
bitr3i.2 (𝜓𝜒)
Assertion
Ref Expression
bitr3i (𝜑𝜒)

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3 (𝜓𝜑)
21bicomi 214 . 2 (𝜑𝜓)
3 bitr3i.2 . 2 (𝜓𝜒)
42, 3bitri 264 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  3bitr3i  290  3bitr3ri  291  xchnxbi  322  ianor  509  orordi  552  orordir  553  anandi  870  anandir  871  trunantru  1522  falnanfal  1525  had0  1541  nic-axALT  1597  sbied  2407  sbidm  2412  sb6a  2446  sbelx  2456  sbco4  2464  mo  2506  2eu6  2556  bm1.1  2605  cbvab  2744  nabbi  2893  r19.41v  3084  r19.41  3085  2ralor  3104  rexcom4a  3221  2reuswap  3404  2reu5  3410  nfcdeq  3426  sbcid  3446  sbcco2  3453  sbc7  3457  sbcie2g  3463  eqsbc3  3469  sbcralt  3504  cbvralcsf  3558  cbvrabcsf  3561  abss  3663  ssab  3664  raldifb  3742  difrab  3893  euelss  3906  sbccsb  3995  vdif0  4028  difrab0eq  4029  ssunsn2  4350  sspr  4357  sstp  4358  uniintsn  4505  brab1  4691  unopab  4719  axrep5  4767  axsep  4771  intexab  4813  reusv2lem4  4863  reusv2  4865  reuxfrd  4884  wefrc  5098  eliunxp  5248  ralxp  5252  rexxp  5253  opelco  5282  reldm0  5332  resieq  5395  iss  5435  imai  5466  cnvsym  5498  intasym  5499  asymref  5500  codir  5504  poirr2  5508  xpdifid  5550  rninxp  5561  tz6.26  5699  wfis2fg  5705  ordelord  5733  ordtri3  5747  dffun3  5887  funopg  5910  fin  6072  f1cnvcnv  6096  funimass4  6234  fnressn  6410  resoprab  6741  mpt22eqb  6754  elrnmpt2res  6759  ov6g  6783  offval  6889  uniuni  6956  dfwe2  6966  orduniorsuc  7015  tfinds2  7048  resiexg  7087  dfopab2  7207  dfoprab3s  7208  fmpt2x  7221  fparlem1  7262  fparlem2  7263  brtpos0  7344  dftpos3  7355  tpostpos  7357  dfrecs3  7454  tz7.48lem  7521  omeu  7650  ercnv  7748  ixp0  7926  xpcomco  8035  xpassen  8039  php  8129  findcard3  8188  ixpfi2  8249  dfsup2  8335  sup0riota  8356  card2on  8444  infeq5i  8518  cnfcom3lem  8585  r1elss  8654  rankxplim  8727  scott0s  8736  aceq1  8925  dfac5lem1  8931  dfac5lem2  8932  kmlem3  8959  kmlem8  8964  kmlem16  8972  cflem  9053  cf0  9058  alephval2  9379  rankcf  9584  r1tskina  9589  wfgru  9623  genpass  9816  psslinpr  9838  ltpsrpr  9915  infm3  10967  nnwos  11740  ioo0  12185  ico0  12206  ioc0  12207  icc0  12208  elfz2nn0  12415  elfzmlbp  12434  sqeqori  12959  hashgt12el  13193  hashgt12el2  13194  cshwidxmod  13530  clim0  14218  divalglem6  15102  isprm2lem  15375  ncoprmlnprm  15417  pceu  15532  prmreclem2  15602  cshwshash  15792  isstruct  15851  xpscf  16207  acsfn2  16305  invsym2  16404  pospo  16954  f1omvdco3  17850  psgnunilem5  17895  efgrelexlemb  18144  gexex  18237  srgrmhm  18517  lssne0  18932  opsrtoslem1  19465  opsrtoslem2  19466  islindf4  20158  mdetunilem8  20406  cpmatmcllem  20504  pmatcollpw2lem  20563  ntreq0  20862  ordtrest2lem  20988  ist0-3  21130  ist1-2  21132  ist1-3  21134  cmpfi  21192  2ndcctbss  21239  ptbasfi  21365  ptcnplem  21405  hausdiag  21429  hauseqlcld  21430  cnmptcom  21462  txflf  21791  tgphaus  21901  metrest  22310  iccpnfcnv  22724  bcth3  23109  volun  23294  dyadmax  23347  vitalilem2  23359  vitalilem3  23360  mbfimaopnlem  23403  itg2leub  23482  dvres2  23657  ellogdm  24366  reasinsin  24604  leibpilem2  24649  ftalem3  24782  dchreq  24964  legso  25475  outpasch  25628  axcontlem2  25826  incistruhgr  25955  usgr2pth0  26642  rusgrnumwwlkslem  26845  frgr3v  27119  4cycl2vnunb  27134  frgrncvvdeqlem2  27144  lnon0  27623  spansncvi  28481  pjssmii  28510  nmlnopgt0i  28826  largei  29096  cvexchlem  29197  xfree  29273  spc2ed  29282  nmo  29297  2reuswap2  29300  fpwrelmapffslem  29481  addeq0  29484  eliccioo  29613  qtophaus  29877  ordtrest2NEWlem  29942  ordtconnlem1  29944  xrge0iifcnv  29953  xrge0iifiso  29955  xrge0iifhom  29957  cntnevol  30265  eulerpartlemgh  30414  ballotlem7  30571  signswch  30612  bnj446  30757  bnj563  30787  bnj110  30902  bnj153  30924  bnj864  30966  bnj865  30967  bnj849  30969  bnj929  30980  bnj1110  31024  derang0  31125  iccllysconn  31206  cvmsss2  31230  elmrsubrn  31391  quad3  31538  axacprim  31558  dftr6  31615  dfpo2  31620  elintfv  31638  opelco3  31652  elima4  31653  setinds2f  31658  elpotr  31660  frins2fg  31718  wzel  31745  wzelOLD  31746  bdayimaon  31817  elfuns  31997  dfiota3  32005  imagesset  32035  lineunray  32229  ellines  32234  hfninf  32268  bj-axrep5  32767  bj-axsep  32768  bj-rexcom4a  32845  bj-snglc  32932  bj-mpt2mptALT  33047  curf  33358  tan2h  33372  poimirlem26  33406  poimirlem27  33407  poimirlem30  33410  poimirlem32  33412  poimir  33413  ovoliunnfl  33422  voliunnfl  33424  ftc1anc  33464  inixp  33494  heibor1lem  33579  csbcom2fi  33905  tsna1  33922  islshpat  34123  lkr0f  34200  lshpsmreu  34215  cvrnbtwn4  34385  ishlat2  34459  islvol5  34684  tendoeq2  35881  dibelval3  36255  mapdpglem3  36783  hdmapglem7a  37038  4rexfrabdioph  37181  dford4  37415  isdomn3  37601  fgraphopab  37607  ifpim123g  37664  ifpbibib  37674  undmrnresiss  37729  cnvssco  37731  iunrelexpuztr  37830  dffrege115  38092  brco2f1o  38150  ntrneiiso  38209  undisjrab  38325  radcnvrat  38333  opelopab4  38587  2sb5nd  38596  un2122  38837  uunT12p4  38850  onfrALTlem5VD  38941  2sb5ndVD  38966  2sb5ndALT  38988  ndisj2  39038  ssabf  39100  abssf  39115  fourierdlem42  40129  smflimlem4  40745  2rmoswap  40947  ndmaovcom  41048  eliunxp2  41877  pgrpgt2nabl  41912  islindeps  42007  lindslinindsimp1  42011  lindslinindsimp2  42017
  Copyright terms: Public domain W3C validator