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  anandi  655  anandir  656  orordi  914  orordir  915  ianor  966  trunantru  1672  falnanfal  1675  had0  1691  nic-axALT  1747  sbied  2556  sbidm  2561  equsb3  2580  elsb3  2583  elsb4  2586  sb6a  2596  sbelx  2606  sbco4  2614  mo  2657  2eu6  2707  bm1.1  2756  cbvab  2895  nabbi  3045  r19.41v  3237  r19.41  3238  2ralor  3257  rexcom4a  3378  2reuswap  3562  2reu5  3568  nfcdeq  3584  sbcid  3604  sbcco2  3611  sbc7  3615  sbcie2g  3621  eqsbc3  3627  sbcralt  3660  cbvralcsf  3714  cbvrabcsf  3717  abss  3820  ssab  3821  raldifb  3901  difrab  4049  euelss  4062  sbccsb  4148  vdif0  4179  difrab0eq  4180  ssunsn2  4493  sspr  4499  sstp  4500  uniintsn  4648  brab1  4834  unopab  4862  axrep5  4910  axsep  4914  intexab  4953  reusv2lem4  5001  reusv2  5003  reuxfrd  5021  wefrc  5243  eliunxp  5398  ralxp  5402  rexxp  5403  opelco  5432  reldm0  5481  resieq  5548  iss  5588  imai  5619  cnvsym  5651  intasym  5652  asymref  5653  codir  5657  poirr2  5661  xpdifid  5703  rninxp  5714  tz6.26  5854  wfis2fg  5860  ordelord  5888  ordtri3  5902  dffun3  6042  funopg  6065  fin  6225  f1cnvcnv  6250  funimass4  6389  fnressn  6568  resoprab  6903  mpt22eqb  6916  elrnmpt2res  6921  ov6g  6945  offval  7051  uniuni  7118  dfwe2  7128  orduniorsuc  7177  tfinds2  7210  resiexg  7249  dfopab2  7371  dfoprab3s  7372  fmpt2x  7386  fparlem1  7428  fparlem2  7429  brtpos0  7511  dftpos3  7522  tpostpos  7524  dfrecs3  7622  tz7.48lem  7689  omeu  7819  ercnv  7917  ixp0  8095  xpcomco  8206  xpassen  8210  php  8300  findcard3  8359  ixpfi2  8420  dfsup2  8506  sup0riota  8527  card2on  8615  infeq5i  8697  cnfcom3lem  8764  r1elss  8833  rankxplim  8906  scott0s  8915  aceq1  9140  dfac5lem1  9146  dfac5lem2  9147  kmlem3  9176  kmlem8  9181  kmlem16  9189  cflem  9270  cf0  9275  alephval2  9596  rankcf  9801  r1tskina  9806  wfgru  9840  genpass  10033  psslinpr  10055  ltpsrpr  10132  infm3  11184  nnwos  11958  ioo0  12405  ico0  12426  ioc0  12427  icc0  12428  elfz2nn0  12638  elfzmlbp  12658  sqeqori  13183  hashgt12el  13412  hashgt12el2  13413  cshwidxmod  13758  clim0  14445  divalglem6  15329  ncoprmlnprm  15643  pceu  15758  prmreclem2  15828  cshwshash  16018  isstruct  16077  xpscf  16434  acsfn2  16531  invsym2  16630  pospo  17181  f1omvdco3  18076  psgnunilem5  18121  efgrelexlemb  18370  gexex  18463  srgrmhm  18744  lssne0  19161  opsrtoslem1  19699  opsrtoslem2  19700  islindf4  20394  mdetunilem8  20643  cpmatmcllem  20743  pmatcollpw2lem  20802  ntreq0  21102  ordtrest2lem  21228  ist0-3  21370  ist1-2  21372  ist1-3  21374  cmpfi  21432  2ndcctbss  21479  ptbasfi  21605  ptcnplem  21645  hausdiag  21669  hauseqlcld  21670  cnmptcom  21702  txflf  22030  tgphaus  22140  metrest  22549  iccpnfcnv  22963  bcth3  23347  volun  23533  dyadmax  23586  vitalilem2  23597  vitalilem3  23598  mbfimaopnlem  23642  itg2leub  23721  dvres2  23896  ellogdm  24606  reasinsin  24844  leibpilem2  24889  ftalem3  25022  dchreq  25204  legso  25715  outpasch  25868  axcontlem2  26066  incistruhgr  26195  nbgrel  26456  usgr2pth0  26896  rusgrnumwwlkslem  27118  frgr3v  27457  4cycl2vnunb  27472  frgrncvvdeqlem2  27482  lnon0  27993  spansncvi  28851  pjssmii  28880  nmlnopgt0i  29196  largei  29466  cvexchlem  29567  xfree  29643  spc2ed  29652  nmo  29665  2reuswap2  29667  fpwrelmapffslem  29847  addeq0  29850  eliccioo  29979  qtophaus  30243  ordtrest2NEWlem  30308  ordtconnlem1  30310  xrge0iifcnv  30319  xrge0iifiso  30321  xrge0iifhom  30323  cntnevol  30631  eulerpartlemgh  30780  ballotlem7  30937  signswch  30978  bnj446  31123  bnj563  31151  bnj110  31266  bnj153  31288  bnj864  31330  bnj865  31331  bnj849  31333  bnj929  31344  bnj1110  31388  derang0  31489  iccllysconn  31570  cvmsss2  31594  elmrsubrn  31755  quad3  31902  axacprim  31922  dftr6  31978  dfpo2  31983  elintfv  32000  opelco3  32014  elima4  32015  setinds2f  32020  elpotr  32022  frins2fg  32084  wzel  32106  bdayimaon  32180  elfuns  32359  dfiota3  32367  imagesset  32397  lineunray  32591  ellines  32596  hfninf  32630  bj-axrep5  33128  bj-axsep  33129  bj-rexcom4a  33199  bj-snglc  33288  bj-mpt2mptALT  33404  curf  33720  tan2h  33734  poimirlem26  33768  poimirlem27  33769  poimirlem30  33772  poimirlem32  33774  poimir  33775  ovoliunnfl  33784  voliunnfl  33786  ftc1anc  33825  inixp  33855  heibor1lem  33940  csbcom2fi  34266  tsna1  34283  anan  34344  brid  34420  idinxpssinxp4  34434  iss2  34454  xrninxp  34492  cossssid3  34561  islshpat  34826  lkr0f  34903  lshpsmreu  34918  cvrnbtwn4  35088  ishlat2  35162  islvol5  35387  tendoeq2  36583  dibelval3  36957  mapdpglem3  37485  hdmapglem7a  37737  4rexfrabdioph  37888  dford4  38122  isdomn3  38308  fgraphopab  38314  ifpim123g  38371  ifpbibib  38381  undmrnresiss  38436  cnvssco  38438  iunrelexpuztr  38537  dffrege115  38798  brco2f1o  38856  ntrneiiso  38915  undisjrab  39031  radcnvrat  39039  opelopab4  39292  2sb5nd  39301  un2122  39542  uunT12p4  39555  2sb5ndVD  39668  2sb5ndALT  39690  ndisj2  39739  ssabf  39801  abssf  39816  fourierdlem42  40883  smflimlem4  41502  2rmoswap  41704  ndmaovcom  41805  eliunxp2  42640  pgrpgt2nabl  42675  islindeps  42770  lindslinindsimp1  42774  lindslinindsimp2  42780
  Copyright terms: Public domain W3C validator