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

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

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2 (𝜑𝜓)
2 bitr4i.2 . . 3 (𝜒𝜓)
32bicomi 214 . 2 (𝜓𝜒)
41, 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:  3bitr2i  288  3bitr2ri  289  3bitr4i  292  3bitr4ri  293  imor  428  dfbi2  659  pm5.32  667  imdistan  724  bianass  841  imimorb  920  nbi2  935  pm5.6  950  mpbiran  952  mpbiran2  953  biluk  973  casesifp  1025  3anrev  1047  an3andi  1443  nancom  1448  nanbi  1452  xorneg  1474  cadan  1546  cadcomb  1550  nic-ax  1596  nic-axALT  1597  nf3  1710  19.43  1808  19.3v  1895  nf5  2114  nf6  2115  sb6x  2382  sb5f  2384  sb3an  2398  sbequ8ALT  2405  sb5  2428  sbhb  2436  sbnf2  2437  sbcom2  2443  eu1  2508  cleqh  2722  clelab  2746  necon3bii  2843  neor  2882  neorian  2885  r2allem  2934  r19.23t  3017  r19.26-3  3062  r19.26m  3063  r19.43  3088  rabid2  3113  rabid2f  3114  eqvf  3199  isset  3202  ralv  3214  rexv  3215  reuv  3216  rmov  3217  rexcom4b  3222  ceqsex4v  3242  ceqsex8v  3244  ceqsrexv  3330  rabtru  3355  ralrab2  3366  rexrab2  3368  reu2  3388  reu3  3390  reueq  3398  2reuswap  3404  reuind  3405  2reu5lem3  3409  sbc3an  3488  rmo2  3519  dfss2  3584  dfss3  3585  dfss3f  3587  ssabral  3665  rabss  3671  ssrabeq  3681  uniiunlem  3683  sspsstri  3701  npss  3709  raldifb  3742  uncom  3749  inass  3815  symdifass  3845  nsspssun  3849  dfss4  3850  dfun2  3851  dfin2  3852  indi  3865  indifdir  3875  difin2  3882  reupick3  3904  eq0f  3917  neq0f  3918  n0fOLD  3920  rabn0  3949  csbab  3999  vss  4003  disj  4008  disj3  4012  undisj1  4020  undisj2  4021  inundif  4037  undif  4040  rabeqsn  4205  rabsssn  4206  exsnrex  4212  euabsn2  4251  euabsn  4252  raldifsni  4315  tppreqb  4327  pwpw0  4335  prssg  4341  ssunsn  4351  pwpr  4421  dfuni2  4429  unissb  4460  elint2  4473  ssint  4484  uniintab  4506  iuneq12df  4535  dfiin2g  4544  iunn0  4571  iunxun  4596  iunxiun  4599  iinpw  4608  disjor  4625  disjxiun  4640  disjxiunOLD  4641  dftr2  4745  dftr5  4746  dftr3  4747  dftr4  4748  vprc  4787  inuni  4817  eusv2  4856  reusv2lem4  4863  rexxfr  4879  snelpw  4904  sspwb  4908  opthneg  4940  pwssun  5010  dfid3  5015  dffr2  5069  opthprc  5157  elxp3  5159  xpiundir  5164  elvv  5167  brinxp2  5170  relsn  5213  reliun  5229  inxp  5243  raliunxp  5250  cnvuni  5298  dm0rn0  5331  elrn  5355  ssdmres  5408  dfres2  5441  dfima2  5456  args  5481  dffr3  5486  cotrg  5495  intasym  5499  asymref  5500  intirr  5502  cnv0OLD  5524  xpnz  5541  xp11  5557  xpimasn  5567  resco  5627  rnco  5629  coiun  5633  coass  5642  cnvso  5662  elsnxp  5665  elsnxpOLD  5666  dffr4  5684  wfi  5701  dflim2  5769  orddif  5808  dfiota2  5840  dffun2  5886  dffun6f  5890  dffun7  5903  dffun9  5905  funfn  5906  svrelfun  5949  mptfnf  6002  dffn2  6034  dffn3  6041  fint  6071  dffn4  6108  dff1o4  6132  brprcneu  6171  eqfnfv3  6299  fnreseql  6313  fsn  6387  ftpg  6408  abrexco  6487  imaiun  6488  dff13  6497  isof1oidb  6559  isof1oopb  6560  isocnv2  6566  mpt22eqb  6754  elovmpt2  6864  sorpss  6927  abexex  7136  elxp6  7185  elxp7  7186  releldm2  7203  opiota  7214  fnmpt2  7223  frxp  7272  cnvimadfsn  7289  mpt2xneldm  7323  dftpos4  7356  wfrlem8  7407  wfrfun  7410  dfrecs3  7454  tfrlem7  7464  ondif1  7566  oarec  7627  oeeu  7668  0er  7765  0erOLD  7766  eroveu  7827  erovlem  7828  map0e  7880  elixpconst  7901  domen  7953  brsdom  7963  brdom2  7970  reuen1  8010  sbthlem10  8064  brsdom2  8069  xpf1o  8107  onfin2  8137  0sdom1dom  8143  modom  8146  unfi  8212  marypha2lem3  8328  wemapsolem  8440  sucprcreg  8491  elom3  8530  dfom5  8532  trcl  8589  epfrs  8592  rankf  8642  scottexs  8735  scott0s  8736  cplem1  8737  karden  8743  hta  8745  pm54.43lem  8810  alephsuc2  8888  iscard3  8901  aceq0  8926  aceq3lem  8928  dfac3  8929  dfac5lem2  8932  dfac5  8936  dfac7  8939  dfac12a  8955  kmlem12  8968  kmlem14  8970  kmlem15  8971  infmap2  9025  ackbij2  9050  dfacfin7  9206  ituniiun  9229  zorng  9311  brdom7disj  9338  entri2  9365  alephreg  9389  fpwwe2lem12  9448  fpwwe2lem13  9449  pwfseqlem1  9465  grutsk  9629  axgroth4  9639  grothprim  9641  grothtsk  9642  elni2  9684  ltsopi  9695  genpass  9816  psslinpr  9838  ltexprlem4  9846  ltresr  9946  1re  10024  infm3  10967  elnnz  11372  dfz2  11380  2rexuz  11725  nnwos  11740  eluz2b1  11744  qexALT  11788  elxr  11935  dflt2  11966  xrsupss  12124  xrinfmss  12125  elixx1  12169  elioo2  12201  elioopnf  12252  elicopnf  12254  elfz1  12316  fznn  12393  fzp1nel  12408  fznn0  12416  preduz  12445  prinfzo0  12490  injresinj  12572  nn0opthlem1  13038  faclbnd4lem1  13063  hashfxnn0  13107  hashfOLD  13109  hashprdifel  13169  hashfun  13207  hashf1  13224  fz1isolem  13228  f1oun2prg  13643  brtrclfv  13724  shftdm  13792  rediv  13852  imdiv  13859  rexanre  14067  caubnd  14079  climreu  14268  prodmo  14647  dvdslelem  15012  3dvdsdec  15035  3dvdsdecOLD  15036  3dvds2dec  15037  3dvds2decOLD  15038  bitsval  15127  smueqlem  15193  algcvgblem  15271  lcmfunsnlem2  15334  isprm2  15376  isprm3  15377  isprm4  15378  pythagtriplem2  15503  elgz  15616  hashbc0  15690  0ram  15705  isstruct  15851  issect  16394  isfull2  16552  isfth2  16556  fucinv  16614  eldmcoa  16696  isdrs  16915  fpwipodrs  17145  submacs  17346  isnsg4  17618  isgim  17685  gaorb  17721  oppgid  17767  oppgsubm  17773  oppgcntz  17775  ispgp  17988  efgsdm  18124  efgcpbllema  18148  iscyg2  18265  isring  18532  isirred2  18682  opprirred  18683  dfrhm2  18698  drngid2  18744  opprsubrg  18782  islmod  18848  lss1d  18944  islmhm  19008  islmim  19043  lbsextlem2  19140  lidlnz  19209  lidldvgen  19236  isnzr2  19244  isassa  19296  dfprm2  19823  isphl  19954  elocv  19993  iunocv  20006  isobs  20045  islinds  20129  1mavmul  20335  isbasis3g  20734  fctop  20789  cctop  20791  isclo2  20873  restsn  20955  lmbr  21043  ist0-3  21130  2ndcdisj  21240  1stccnp  21246  islocfin  21301  1stckgenlem  21337  txbas  21351  ptbasin  21361  tx2cn  21394  fbfinnfr  21626  fbasrn  21669  filuni  21670  ufinffr  21714  fin1aufil  21717  rnelfmlem  21737  flimrest  21768  alexsubALTlem3  21834  alexsubALTlem4  21835  tgphaus  21901  istlm  21969  iscusp2  22087  metuel2  22351  isngp2  22382  isnlm  22460  elcncf1di  22679  isphtpc  22774  phtpcer  22775  phtpcerOLD  22776  om1elbas  22813  isclm  22845  iscvsp  22909  iscph  22951  iscau3  23057  minveclem3b  23180  elovolm  23224  ioombl1lem4  23310  dyaddisj  23345  vitali  23363  itg1climres  23462  itg2seq  23490  itg2monolem1  23498  itg2mono  23501  limcrcl  23619  lhop1  23758  itgsubst  23793  mdegleb  23805  isuc1p  23881  ismon1p  23883  plydivex  24033  ellogdm  24366  1cubr  24550  atandm2  24585  birthdaylem3  24661  dmarea  24665  dchrelbas2  24943  dchrelbas4  24949  axcontlem7  25831  nb3grpr  26265  nb3grpr2  26266  upgrwlkcompim  26520  wlkson  26533  wlkonprop  26535  wksonproplem  26582  ispth  26600  wwlknon  26723  wwlksnextinj  26775  elwspths2spth  26843  rusgrnumwwlkl1  26844  erclwwlksref  26914  frgr3v  27119  nmoubi  27597  nmobndseqi  27604  nmobndseqiALT  27605  minvecolem1  27700  isch2  28050  hlimreui  28066  isch3  28068  ocsh  28112  dfch2  28236  spanuni  28373  nonbooli  28480  5oalem7  28489  adjsym  28662  elbdop2  28700  dmadjss  28716  nmopub  28737  nmfnleub  28754  nmop0h  28820  pjssposi  29001  pjordi  29002  cvbr2  29112  cvnbtwn2  29116  mdsl2i  29151  cvmdi  29153  elat2  29169  atom1d  29182  chirredi  29223  cdj3i  29270  or3di  29277  moel  29295  mo5f  29296  2reuswap2  29300  rexunirn  29303  difrab2  29311  difininv  29326  iuneq12daf  29345  iuninc  29351  disjorf  29364  disjunsn  29379  rabfmpunirn  29426  aciunf1  29436  funcnv5mpt  29443  dfrp2  29506  eliccelico  29513  elicoelioo  29514  isomnd  29675  omndmul2  29686  isslmd  29729  hasheuni  30121  pwsiga  30167  sigainb  30173  issros  30212  2ndmbfm  30297  omssubaddlem  30335  omssubadd  30336  sitgaddlemb  30384  eulerpartlemgvv  30412  eulerpartlemn  30417  probun  30455  ballotlem2  30524  ballotlemodife  30533  bnj252  30743  bnj253  30744  bnj255  30745  bnj345  30754  bnj133  30767  bnj976  30822  bnj1098  30828  bnj121  30914  bnj130  30918  bnj150  30920  bnj581  30952  bnj607  30960  bnj865  30967  bnj917  30978  bnj934  30979  bnj964  30987  bnj983  30995  bnj996  30999  bnj1021  31008  bnj1033  31011  bnj1047  31015  bnj1049  31016  bnj1090  31021  bnj1128  31032  bnj1175  31046  bnj1189  31051  bnj1253  31059  bnj1312  31100  erdszelem9  31155  erdszelem10  31156  pconnconn  31187  cvmliftiota  31257  elmthm  31447  nepss  31574  dfso2  31619  dfpo2  31620  dfres3  31624  elrn3  31628  imaindm  31656  elpotr  31660  dfon2lem5  31666  dfon2lem7  31668  dfon2lem8  31669  frind  31714  soseq  31725  elwlim  31743  elwlimOLD  31744  wzel  31745  wzelOLD  31746  frrlem5c  31760  elno3  31782  nosgnn0  31785  nosepon  31792  nocvxminlem  31867  scutcut  31886  scutbday  31887  dmscut  31892  scutf  31893  sltrec  31898  brtxp2  31963  brpprod3a  31968  eltrans  31973  dfon3  31974  dffix2  31987  dffun10  31996  elfuns  31997  brsingle  31999  brimg  32019  funpartfun  32025  funpartfv  32027  cgrxfr  32137  segletr  32196  outsideoftr  32211  neifg  32341  filnetlem4  32351  df3nandALT1  32371  bj-consensusALT  32538  bj-biexal3  32673  bj-sb5  32743  bj-ralvw  32840  bj-rexvwv  32841  bj-rexcom4bv  32846  bj-rexcom4b  32847  bj-sbeq  32871  bj-inrab  32898  bj-xpima1snALT  32919  bj-dfmpt2a  33046  topdifinffinlem  33166  topdifinfeq  33169  relowlssretop  33182  relowlpssretop  33183  rdgeqoa  33189  wl-dfnan2  33267  wl-nannan  33269  rabiun  33353  phpreu  33364  fin2solem  33366  matunitlindflem2  33377  ptrest  33379  poimirlem25  33405  poimirlem27  33407  poimirlem30  33410  ismblfin  33421  ovoliunnfl  33422  voliunnfl  33424  volsupnfl  33425  itg2addnclem2  33433  fdc  33512  prdstotbnd  33564  isdrngo1  33726  ispridl  33804  ismaxidl  33810  impor  33851  selconj  33873  tradd  33878  scott0f  33948  prter1  33983  islshp  34085  islshpat  34123  lcvbr2  34128  lcvnbtwn2  34133  cvrnbtwn3  34382  isatl  34405  ishlat1  34458  ishlat2  34459  cvrat4  34548  pmapglbx  34874  lhpexle3  35117  dib1dim  36273  diblsmopel  36279  lcfls1lem  36642  rexrabdioph  37177  dford4  37415  issdrg  37586  isdomn3  37601  ifpdfor2  37624  ifpdfan2  37626  ifpdfor  37628  ifpdfan  37629  ifpdfbi  37637  ifpnot23b  37646  ifpnot23c  37648  ifpnot23d  37649  ifpim123g  37664  ifpbibib  37674  clss2lem  37737  imaiun1  37762  coiun1  37763  brfvrcld2  37803  iunrelexp0  37813  brtrclfv2  37838  snhesn  37900  dffrege76  38053  frege97  38074  frege98  38075  frege109  38086  frege110  38087  dffrege115  38092  frege131  38108  frege133  38110  ntrneineine1lem  38202  ntrneiel2  38204  ntrneiiso  38209  gneispace3  38251  pm11.52  38406  pm11.58  38410  pm13.192  38431  conss34OLD  38466  impexpdcom  38541  sbc3or  38558  opelopab4  38587  uunT12p1  38847  uunT12p2  38848  uunT12p3  38849  uun2221  38860  uun2221p1  38861  uun2221p2  38862  undif3VD  38938  onfrALTlem5VD  38941  ndisj2  39038  nssrex  39080  rabssf  39122  bothtbothsame  40829  bothfbothsame  40830  aiffbtbat  40838  rmoanim  40942  2rmoswap  40947  dfodd2  41314  dfeven5  41343  dfodd7  41344  1nevenALTV  41367  oddprmne2  41389  isrng  41641  isrnghm  41657  islindeps2  42037  isldepslvec2  42039  setrec1lem3  42201  aacllem  42312
  Copyright terms: Public domain W3C validator