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

Theorem bitr3i 265
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 213 . 2 (𝜑𝜓)
3 bitr3i.2 . 2 (𝜓𝜒)
42, 3bitri 263 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  3bitrri  286  3bitr3i  289  3bitr3ri  290  xchnxbi  321  ianor  508  orordi  551  orordir  552  anandi  867  anandir  868  trunantru  1515  falnanfal  1518  had0  1534  nic-axALT  1590  sbied  2397  sbidm  2402  sb6a  2436  sbelx  2446  sbco4  2454  mo  2496  2eu6  2546  bm1.1  2595  cbvab  2733  nabbi  2884  r19.41v  3070  r19.41  3071  2ralor  3088  rexcom4a  3199  2reuswap  3377  2reu5  3383  nfcdeq  3399  sbcid  3419  sbcco2  3426  sbc7  3430  sbcie2g  3436  eqsbc3  3442  sbcralt  3477  cbvralcsf  3531  cbvrabcsf  3534  abss  3634  ssab  3635  raldifb  3712  difrab  3860  euelss  3873  sbccsb  3956  vdif0  3989  difrab0eq  3990  ssunsn2  4299  sspr  4306  sstp  4307  uniintsn  4449  brab1  4630  unopab  4660  axrep5  4704  axsep  4708  intexab  4749  reusv2lem4  4798  reusv2  4800  reuxfrd  4819  wefrc  5032  eliunxp  5181  ralxp  5185  rexxp  5186  opelco  5215  reldm0  5264  resieq  5327  iss  5367  imai  5397  cnvsym  5429  intasym  5430  asymref  5431  codir  5435  poirr2  5439  xpdifid  5481  rninxp  5492  tz6.26  5628  wfis2fg  5634  ordelord  5662  ordtri3  5676  dffun3  5815  funopg  5836  fin  5998  f1cnvcnv  6022  funimass4  6157  fnressn  6330  resoprab  6654  mpt22eqb  6667  elrnmpt2res  6672  ov6g  6696  offval  6802  uniuni  6865  dfwe2  6873  orduniorsuc  6922  tfinds2  6955  resiexg  6994  dfopab2  7113  dfoprab3s  7114  fmpt2x  7125  fparlem1  7164  fparlem2  7165  brtpos0  7246  dftpos3  7257  tpostpos  7259  dfrecs3  7356  tz7.48lem  7423  omeu  7552  ercnv  7650  ixp0  7827  xpcomco  7935  xpassen  7939  php  8029  findcard3  8088  ixpfi2  8147  dfsup2  8233  sup0riota  8254  card2on  8342  infeq5i  8416  cnfcom3lem  8483  r1elss  8552  rankxplim  8625  scott0s  8634  aceq1  8823  dfac5lem1  8829  dfac5lem2  8830  kmlem3  8857  kmlem8  8862  kmlem16  8870  cflem  8951  cf0  8956  alephval2  9273  rankcf  9478  r1tskina  9483  wfgru  9517  genpass  9710  psslinpr  9732  ltpsrpr  9809  infm3  10861  nnwos  11631  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  elfz2nn0  12300  elfzmlbp  12319  sqeqori  12838  hashgt12el  13070  hashgt12el2  13071  cshwidxmod  13400  clim0  14085  divalglem6  14959  isprm2lem  15232  ncoprmlnprm  15274  pceu  15389  prmreclem2  15459  cshwshash  15649  isstruct  15705  xpscf  16049  acsfn2  16147  invsym2  16246  pospo  16796  f1omvdco3  17692  psgnunilem5  17737  efgrelexlemb  17986  gexex  18079  srgrmhm  18359  lssne0  18772  opsrtoslem1  19305  opsrtoslem2  19306  islindf4  19996  mdetunilem8  20244  cpmatmcllem  20342  pmatcollpw2lem  20401  ntreq0  20691  ordtrest2lem  20817  ist0-3  20959  ist1-2  20961  ist1-3  20963  cmpfi  21021  2ndcctbss  21068  ptbasfi  21194  ptcnplem  21234  hausdiag  21258  hauseqlcld  21259  cnmptcom  21291  txflf  21620  tgphaus  21730  metrest  22139  iccpnfcnv  22551  bcth3  22936  volun  23120  dyadmax  23172  vitalilem2  23184  vitalilem3  23185  mbfimaopnlem  23228  itg2leub  23307  dvres2  23482  ellogdm  24185  reasinsin  24423  leibpilem2  24468  ftalem3  24601  dchreq  24783  legso  25294  outpasch  25447  axcontlem2  25645  incistruhgr  25746  rusgranumwlklem0  26475  frgra3v  26529  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  usg2spot2nb  26592  lnon0  27037  spansncvi  27895  pjssmii  27924  nmlnopgt0i  28240  largei  28510  cvexchlem  28611  xfree  28687  spc2ed  28696  nmo  28709  2reuswap2  28712  fpwrelmapffslem  28895  addeq0  28898  eliccioo  28970  qtophaus  29231  ordtrest2NEWlem  29296  ordtconlem1  29298  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  cntnevol  29618  eulerpartlemgh  29767  ballotlem7  29924  signswch  29964  bnj446  30036  bnj563  30067  bnj110  30182  bnj153  30204  bnj864  30246  bnj865  30247  bnj849  30249  bnj929  30260  bnj1110  30304  derang0  30405  iccllyscon  30486  cvmsss2  30510  elmrsubrn  30671  quad3  30818  axacprim  30838  dftr6  30893  dfpo2  30898  opelco3  30923  elima4  30924  setinds2f  30928  elpotr  30930  frins2fg  30988  wzel  31015  wzelOLD  31016  nobndlem1  31091  elfuns  31192  dfiota3  31200  imagesset  31230  lineunray  31424  ellines  31429  hfninf  31463  bj-axrep5  31980  bj-axsep  31981  bj-rexcom4a  32064  bj-snglc  32150  bj-mpt2mptALT  32253  curf  32557  tan2h  32571  poimirlem26  32605  poimirlem27  32606  poimirlem30  32609  poimirlem32  32611  poimir  32612  ovoliunnfl  32621  voliunnfl  32623  ftc1anc  32663  inixp  32693  heibor1lem  32778  csbcom2fi  33104  tsna1  33121  islshpat  33322  lkr0f  33399  lshpsmreu  33414  cvrnbtwn4  33584  ishlat2  33658  islvol5  33883  tendoeq2  35080  dibelval3  35454  mapdpglem3  35982  hdmapglem7a  36237  4rexfrabdioph  36380  dford4  36614  isdomn3  36801  fgraphopab  36807  ifpim123g  36864  ifpbibib  36874  undmrnresiss  36929  cnvssco  36931  iunrelexpuztr  37030  dffrege115  37292  brco2f1o  37350  ntrneiiso  37409  undisjrab  37527  radcnvrat  37535  opelopab4  37788  2sb5nd  37797  un2122  38038  uunT12p4  38051  onfrALTlem5VD  38143  2sb5ndVD  38168  2sb5ndALT  38190  ndisj2  38243  ssabf  38308  abssf  38326  fourierdlem42  39042  smflimlem4  39660  2rmoswap  39833  ndmaovcom  39934  usgr2pth0  40971  frgr3v  41445  4cycl2vnunb-av  41460  fusgr2wsp2nb  41498  eliunxp2  41905  pgrpgt2nabl  41941  islindeps  42036  lindslinindsimp1  42040  lindslinindsimp2  42046
  Copyright terms: Public domain W3C validator