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

Theorem bitr3i 268
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 215 . 2 (𝜑𝜓)
3 bitr3i.2 . 2 (𝜓𝜒)
42, 3bitri 266 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  3bitrri  289  3bitr3i  292  3bitr3ri  293  xchnxbi  323  an12  627  anandi  658  anandir  659  orordi  943  orordir  944  ianor  995  trunantru  1679  falnanfal  1682  had0  1698  nic-axALT  1754  sbied  2568  sbidm  2573  equsb3  2592  elsb3  2595  elsb4  2598  sb6a  2608  sbelx  2618  sbco4  2626  mo  2671  2eu6  2722  bm1.1OLD  2790  cbvab  2930  nabbi  3080  r19.41v  3277  r19.41  3278  2ralor  3297  rexcom4a  3420  2reuswap  3608  2reu5  3614  nfcdeq  3630  sbcid  3650  sbcco2  3657  sbc7  3661  sbcie2g  3667  eqsbc3  3673  sbcralt  3706  cbvralcsf  3760  cbvrabcsf  3763  abss  3868  ssab  3869  raldifb  3949  difrab  4102  euelss  4115  sbccsb  4202  vdif0  4233  difrab0eq  4234  ssunsn2  4548  sspr  4554  sstp  4555  uniintsn  4706  brab1  4892  unopab  4922  axrep5  4970  axsep  4974  intexab  5014  reusv2lem4  5070  reusv2  5072  reuxfrd  5090  wefrc  5305  eliunxp  5461  ralxp  5465  rexxp  5466  opelco  5495  reldm0  5544  resieq  5611  iss  5652  elridOLD  5663  imai  5688  cnvsym  5721  intasym  5722  asymref  5723  codir  5727  poirr2  5731  xpdifid  5773  rninxp  5784  tz6.26  5924  wfis2fg  5930  ordelord  5958  ordtri3  5972  dffun3  6108  funopg  6131  fin  6296  f1cnvcnv  6321  funimass4  6464  fnressn  6645  resoprab  6982  mpt22eqb  6995  elrnmpt2res  7000  ov6g  7024  offval  7130  uniuni  7197  dfwe2  7207  orduniorsuc  7256  tfinds2  7289  resiexg  7328  dfopab2  7450  dfoprab3s  7451  fmpt2x  7465  fparlem1  7507  fparlem2  7508  brtpos0  7590  dftpos3  7601  tpostpos  7603  dfrecs3  7701  tz7.48lem  7768  omeu  7898  ercnv  7996  ixp0  8174  xpcomco  8285  xpassen  8289  php  8379  findcard3  8438  ixpfi2  8499  dfsup2  8585  sup0riota  8606  card2on  8694  infeq5i  8776  cnfcom3lem  8843  r1elss  8912  rankxplim  8985  scott0s  8994  aceq1  9219  dfac5lem1  9225  dfac5lem2  9226  kmlem3  9255  kmlem8  9260  kmlem16  9268  cflem  9349  cf0  9354  alephval2  9675  fpwwe2lem8  9740  fpwwe2lem12  9744  rankcf  9880  r1tskina  9885  wfgru  9919  genpass  10112  psslinpr  10134  ltpsrpr  10211  infm3  11263  nnwos  11970  ioo0  12414  ico0  12435  ioc0  12436  icc0  12437  elfz2nn0  12650  elfzmlbp  12670  sqeqori  13195  hashgt12el  13423  hashgt12el2  13424  cshwidxmod  13769  clim0  14456  divalglem6  15337  ncoprmlnprm  15649  pceu  15764  prmreclem2  15834  cshwshash  16019  xpscf  16427  acsfn2  16524  invsym2  16623  pospo  17174  f1omvdco3  18066  psgnunilem5  18111  efgrelexlemb  18360  gexex  18453  srgrmhm  18734  lssne0  19151  opsrtoslem1  19688  opsrtoslem2  19689  islindf4  20383  mdetunilem8  20632  cpmatmcllem  20732  pmatcollpw2lem  20791  ntreq0  21091  ordtrest2lem  21217  ist0-3  21359  ist1-2  21361  ist1-3  21363  cmpfi  21421  2ndcctbss  21468  ptbasfi  21594  ptcnplem  21634  hausdiag  21658  hauseqlcld  21659  cnmptcom  21691  txflf  22019  tgphaus  22129  metrest  22538  iccpnfcnv  22952  bcth3  23336  volun  23522  dyadmax  23575  vitalilem2  23586  vitalilem3  23587  mbfimaopnlem  23632  itg2leub  23711  dvres2  23886  ellogdm  24595  reasinsin  24833  leibpilem2  24878  ftalem3  25011  dchreq  25193  legso  25704  outpasch  25857  axcontlem2  26055  incistruhgr  26184  nbgrel  26445  usgr2pth0  26885  rusgrnumwwlkslem  27107  frgr3v  27446  4cycl2vnunb  27461  frgrncvvdeqlem2  27471  lnon0  27977  spansncvi  28835  pjssmii  28864  nmlnopgt0i  29180  largei  29450  cvexchlem  29551  xfree  29627  spc2ed  29636  nmo  29649  2reuswap2  29650  fpwrelmapffslem  29830  addeq0  29833  eliccioo  29960  qtophaus  30224  ordtrest2NEWlem  30289  ordtconnlem1  30291  xrge0iifcnv  30300  xrge0iifiso  30302  xrge0iifhom  30304  cntnevol  30612  eulerpartlemgh  30761  ballotlem7  30918  signswch  30959  bnj446  31104  bnj563  31131  bnj110  31246  bnj153  31268  bnj864  31310  bnj865  31311  bnj849  31313  bnj929  31324  bnj1110  31368  derang0  31469  iccllysconn  31550  cvmsss2  31574  elmrsubrn  31735  quad3  31881  axacprim  31901  dftr6  31957  dfpo2  31962  elintfv  31979  opelco3  31993  elima4  31994  setinds2f  31999  elpotr  32001  frins2fg  32063  wzel  32085  bdayimaon  32159  elfuns  32338  dfiota3  32346  imagesset  32376  lineunray  32570  ellines  32575  hfninf  32609  bj-axrep5  33101  bj-axsep  33102  bj-rexcom4a  33173  bj-snglc  33262  bj-mpt2mptALT  33378  curf  33695  tan2h  33709  poimirlem26  33743  poimirlem27  33744  poimirlem30  33747  poimirlem32  33749  poimir  33750  ovoliunnfl  33759  voliunnfl  33761  ftc1anc  33800  inixp  33830  heibor1lem  33914  csbcom2fi  34239  tsna1  34256  anan  34315  brid  34388  idinxpssinxp4  34401  iss2  34420  xrninxp  34458  cossssid3  34527  islshpat  34792  lkr0f  34869  lshpsmreu  34884  cvrnbtwn4  35054  ishlat2  35128  islvol5  35354  tendoeq2  36549  dibelval3  36922  mapdpglem3  37450  hdmapglem7a  37702  4rexfrabdioph  37858  dford4  38091  isdomn3  38277  fgraphopab  38283  ifpim123g  38339  ifpbibib  38349  undmrnresiss  38404  cnvssco  38406  iunrelexpuztr  38505  dffrege115  38766  brco2f1o  38824  ntrneiiso  38883  undisjrab  38999  radcnvrat  39007  opelopab4  39259  2sb5nd  39268  un2122  39508  uunT12p4  39521  2sb5ndVD  39634  2sb5ndALT  39656  ndisj2  39705  ssabf  39767  abssf  39781  fourierdlem42  40839  smflimlem4  41458  aiotaexaiotaiota  41670  2rmoswap  41690  ndmaovcom  41788  dmafv2rnb  41812  afv2ndeffv0  41843  eliunxp2  42674  pgrpgt2nabl  42709  islindeps  42804  lindslinindsimp1  42808  lindslinindsimp2  42814
  Copyright terms: Public domain W3C validator