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  321  ianor  508  orordi  551  orordir  552  anandi  888  anandir  889  trunantru  1564  falnanfal  1567  had0  1583  nic-axALT  1639  sbied  2437  sbidm  2442  sb6a  2476  sbelx  2486  sbco4  2494  mo  2537  2eu6  2587  bm1.1  2636  cbvab  2775  nabbi  2925  r19.41v  3118  r19.41  3119  2ralor  3138  rexcom4a  3257  2reuswap  3443  2reu5  3449  nfcdeq  3465  sbcid  3485  sbcco2  3492  sbc7  3496  sbcie2g  3502  eqsbc3  3508  sbcralt  3543  cbvralcsf  3598  cbvrabcsf  3601  abss  3704  ssab  3705  raldifb  3783  difrab  3934  euelss  3947  sbccsb  4037  vdif0  4070  difrab0eq  4071  ssunsn2  4391  sspr  4398  sstp  4399  uniintsn  4546  brab1  4733  unopab  4761  axrep5  4809  axsep  4813  intexab  4852  reusv2lem4  4902  reusv2  4904  reuxfrd  4923  wefrc  5137  eliunxp  5292  ralxp  5296  rexxp  5297  opelco  5326  reldm0  5375  resieq  5442  iss  5482  imai  5513  cnvsym  5545  intasym  5546  asymref  5547  codir  5551  poirr2  5555  xpdifid  5597  rninxp  5608  tz6.26  5749  wfis2fg  5755  ordelord  5783  ordtri3  5797  dffun3  5937  funopg  5960  fin  6123  f1cnvcnv  6147  funimass4  6286  fnressn  6465  resoprab  6798  mpt22eqb  6811  elrnmpt2res  6816  ov6g  6840  offval  6946  uniuni  7013  dfwe2  7023  orduniorsuc  7072  tfinds2  7105  resiexg  7144  dfopab2  7266  dfoprab3s  7267  fmpt2x  7281  fparlem1  7322  fparlem2  7323  brtpos0  7404  dftpos3  7415  tpostpos  7417  dfrecs3  7514  tz7.48lem  7581  omeu  7710  ercnv  7808  ixp0  7983  xpcomco  8091  xpassen  8095  php  8185  findcard3  8244  ixpfi2  8305  dfsup2  8391  sup0riota  8412  card2on  8500  infeq5i  8571  cnfcom3lem  8638  r1elss  8707  rankxplim  8780  scott0s  8789  aceq1  8978  dfac5lem1  8984  dfac5lem2  8985  kmlem3  9012  kmlem8  9017  kmlem16  9025  cflem  9106  cf0  9111  alephval2  9432  rankcf  9637  r1tskina  9642  wfgru  9676  genpass  9869  psslinpr  9891  ltpsrpr  9968  infm3  11020  nnwos  11793  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  elfz2nn0  12469  elfzmlbp  12489  sqeqori  13016  hashgt12el  13248  hashgt12el2  13249  cshwidxmod  13595  clim0  14281  divalglem6  15168  ncoprmlnprm  15483  pceu  15598  prmreclem2  15668  cshwshash  15858  isstruct  15917  xpscf  16273  acsfn2  16371  invsym2  16470  pospo  17020  f1omvdco3  17915  psgnunilem5  17960  efgrelexlemb  18209  gexex  18302  srgrmhm  18582  lssne0  18999  opsrtoslem1  19532  opsrtoslem2  19533  islindf4  20225  mdetunilem8  20473  cpmatmcllem  20571  pmatcollpw2lem  20630  ntreq0  20929  ordtrest2lem  21055  ist0-3  21197  ist1-2  21199  ist1-3  21201  cmpfi  21259  2ndcctbss  21306  ptbasfi  21432  ptcnplem  21472  hausdiag  21496  hauseqlcld  21497  cnmptcom  21529  txflf  21857  tgphaus  21967  metrest  22376  iccpnfcnv  22790  bcth3  23174  volun  23359  dyadmax  23412  vitalilem2  23423  vitalilem3  23424  mbfimaopnlem  23467  itg2leub  23546  dvres2  23721  ellogdm  24430  reasinsin  24668  leibpilem2  24713  ftalem3  24846  dchreq  25028  legso  25539  outpasch  25692  axcontlem2  25890  incistruhgr  26019  nbgrel  26278  usgr2pth0  26717  rusgrnumwwlkslem  26936  frgr3v  27255  4cycl2vnunb  27270  frgrncvvdeqlem2  27280  lnon0  27781  spansncvi  28639  pjssmii  28668  nmlnopgt0i  28984  largei  29254  cvexchlem  29355  xfree  29431  spc2ed  29440  nmo  29453  2reuswap2  29455  fpwrelmapffslem  29635  addeq0  29638  eliccioo  29767  qtophaus  30031  ordtrest2NEWlem  30096  ordtconnlem1  30098  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  cntnevol  30419  eulerpartlemgh  30568  ballotlem7  30725  signswch  30766  bnj446  30911  bnj563  30939  bnj110  31054  bnj153  31076  bnj864  31118  bnj865  31119  bnj849  31121  bnj929  31132  bnj1110  31176  derang0  31277  iccllysconn  31358  cvmsss2  31382  elmrsubrn  31543  quad3  31690  axacprim  31710  dftr6  31766  dfpo2  31771  elintfv  31788  opelco3  31802  elima4  31803  setinds2f  31808  elpotr  31810  frins2fg  31872  wzel  31894  bdayimaon  31968  elfuns  32147  dfiota3  32155  imagesset  32185  lineunray  32379  ellines  32384  hfninf  32418  bj-axrep5  32917  bj-axsep  32918  bj-rexcom4a  32995  bj-snglc  33082  bj-mpt2mptALT  33197  curf  33517  tan2h  33531  poimirlem26  33565  poimirlem27  33566  poimirlem30  33569  poimirlem32  33571  poimir  33572  ovoliunnfl  33581  voliunnfl  33583  ftc1anc  33623  inixp  33653  heibor1lem  33738  csbcom2fi  34064  tsna1  34081  anan  34142  brid  34218  idinxpssinxp4  34232  iss2  34252  xrninxp  34290  cossssid3  34359  islshpat  34622  lkr0f  34699  lshpsmreu  34714  cvrnbtwn4  34884  ishlat2  34958  islvol5  35183  tendoeq2  36379  dibelval3  36753  mapdpglem3  37281  hdmapglem7a  37536  4rexfrabdioph  37679  dford4  37913  isdomn3  38099  fgraphopab  38105  ifpim123g  38162  ifpbibib  38172  undmrnresiss  38227  cnvssco  38229  iunrelexpuztr  38328  dffrege115  38589  brco2f1o  38647  ntrneiiso  38706  undisjrab  38822  radcnvrat  38830  opelopab4  39084  2sb5nd  39093  un2122  39334  uunT12p4  39347  2sb5ndVD  39460  2sb5ndALT  39482  ndisj2  39532  ssabf  39594  abssf  39609  fourierdlem42  40684  smflimlem4  41303  2rmoswap  41505  ndmaovcom  41606  eliunxp2  42437  pgrpgt2nabl  42472  islindeps  42567  lindslinindsimp1  42571  lindslinindsimp2  42577
  Copyright terms: Public domain W3C validator