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

Theorem syl5bi 232
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)
Hypotheses
Ref Expression
syl5bi.1 (𝜑𝜓)
syl5bi.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bi (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3 (𝜑𝜓)
21biimpi 206 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  3imtr4g  285  ancomsd  470  3jao  1388  nfimdOLDOLD  1823  axc16nf  2136  ax13  2248  2euex  2543  2eu1  2552  eqneqall  2804  necon3bd  2807  pm2.61dne  2879  elnelall  2909  spcimgft  3282  rspc  3301  rspcimdv  3308  rspc2gv  3319  euind  3391  reuind  3409  sbciegft  3464  rspsbc  3516  ssexnelpss  3718  ralnralall  4078  pwpw0  4342  sssn  4356  eqsnOLD  4360  prel12  4381  prnebg  4387  pwsnALT  4427  intss1  4490  intmin  4495  uniintsn  4512  iinss  4569  iinss2  4570  disji2  4634  disjiun  4638  disjiund  4641  disjxiun  4647  disjxiunOLD  4648  trel3  4758  trin  4761  trintssOLD  4768  eusvnfb  4860  reusv3  4874  copsexg  4954  propeqop  4968  otiunsndisj  4978  iunopeqop  4979  po3nr  5047  fri  5074  wefrc  5106  wereu2  5109  ssrelrel  5218  relop  5270  iss  5445  restidsingOLD  5457  poirr2  5518  xpcan  5568  xpcan2  5569  sossfld  5578  wfi  5711  wfis2fg  5715  onfr  5761  onmindif  5813  funopg  5920  funssres  5928  funun  5930  fv3  6204  fvmptt  6298  iinpreima  6343  fvn0ssdmfun  6348  dff3  6370  dff4  6371  fmptsng  6431  fmptsnd  6432  tpres  6463  fnprb  6469  fntpb  6470  fvclss  6497  fpropnf1  6521  isomin  6584  isofrlem  6587  weniso  6601  oprabid  6674  ssorduni  6982  onmindif2  7009  limuni3  7049  tfis2f  7052  tfinds  7056  tfinds2  7060  tfinds3  7061  funcnvuni  7116  f1oweALT  7149  f1o2ndf1  7282  poxp  7286  soxp  7287  fnse  7291  suppimacnv  7303  mpt2xopynvov0g  7337  reldmtpos  7357  rntpos  7362  wfrlem14  7425  wfrlem15  7426  onfununi  7435  smoiun  7455  tfrlem1  7469  tfr3  7492  frsucmptn  7531  tz7.49  7537  oaordi  7623  oawordeulem  7631  omeulem1  7659  oeordi  7664  oelimcl  7677  nnaordi  7695  nneob  7729  omsmolem  7730  erdisj  7791  qsss  7805  uniinqs  7824  map0g  7894  resixpfo  7943  ixpsnf1o  7945  xpdom3  8055  mapdom3  8129  phplem4  8139  php3  8143  unxpdomlem3  8163  ssfi  8177  findcard2  8197  findcard3  8200  frfi  8202  isfiniteg  8217  xpfi  8228  fiint  8234  finsschain  8270  dffi2  8326  marypha1lem  8336  marypha2  8342  supmo  8355  suplub2  8364  infmo  8398  ordiso2  8417  ordtypelem7  8426  ordtypelem8  8427  brwdom2  8475  unxpwdom2  8490  ixpiunwdom  8493  elirrv  8501  suc11reg  8513  noinfep  8554  cantnfle  8565  cantnflem1  8583  cantnf  8587  trcl  8601  epfrs  8604  rankpwi  8683  rankunb  8710  rankuni2b  8713  rankxplim3  8741  cplem1  8749  karden  8755  carddom2  8800  fseqenlem2  8845  ac10ct  8854  acni2  8866  acndom  8871  infpwfien  8882  alephordi  8894  alephord  8895  iunfictbso  8934  aceq3lem  8940  dfac5  8948  dfac2  8950  dfac12lem3  8964  dfac12r  8965  cdainflem  9010  cdainf  9011  cfub  9068  cfeq0  9075  coflim  9080  cfslb2n  9087  cofsmo  9088  coftr  9092  infpssr  9127  fin23lem7  9135  fin23lem11  9136  fin23lem21  9158  isf32lem2  9173  isf34lem4  9196  isfin1-2  9204  isfin1-3  9205  fin1a2lem9  9227  fin1a2lem11  9229  fin1a2lem12  9230  fin1a2lem13  9231  domtriomlem  9261  axdc3lem2  9270  axcclem  9276  ac6c4  9300  zorn2lem4  9318  zorn2lem5  9319  zorn2lem7  9321  ttukeylem5  9332  ttukeyg  9336  brdom6disj  9351  fnrndomg  9355  iunfo  9358  iundom2g  9359  ficard  9384  konigthlem  9387  alephval2  9391  pwcfsdom  9402  fpwwe2lem9  9457  fpwwe2lem11  9459  fpwwe2lem12  9460  fpwwe2lem13  9461  pwfseqlem3  9479  gchpwdom  9489  winalim2  9515  gchina  9518  wunex2  9557  tskr1om2  9587  tskxpss  9591  inar1  9594  tskuni  9602  gruun  9625  grudomon  9636  grur1  9639  ltmpi  9723  ltexprlem2  9856  ltexprlem6  9860  reclem2pr  9867  reclem3pr  9868  reclem4pr  9869  suplem1pr  9871  mulgt0sr  9923  supsrlem  9929  axrrecex  9981  axpre-sup  9987  ltlen  10135  addid0  10447  negn0  10456  negf1o  10457  mulge0b  10890  supaddc  10987  supadd  10988  supmul1  10989  supmullem1  10990  supmullem2  10991  supmul  10992  cju  11013  nnsub  11056  0mnnnnn0  11322  un0addcl  11323  un0mulcl  11324  nn0sub  11340  nn0n0n1ge2b  11356  peano5uzi  11463  eluzuzle  11693  zsupss  11774  qbtwnre  12027  xrsupexmnf  12132  xrinfmexpnf  12133  xrsupsslem  12134  xrinfmsslem  12135  xrub  12139  supxrun  12143  ixxdisj  12187  icodisj  12294  difreicc  12301  uzsubsubfz  12360  fzadd2  12373  elfzmlbp  12446  fzofzim  12510  elfznelfzo  12569  injresinj  12584  subfzo0  12585  flval3  12611  modirr  12736  modsumfzodifsn  12738  addmodlteq  12740  ssnn0fi  12779  seqf1o  12837  expcl2lem  12867  expnegz  12889  expaddz  12899  expmulz  12901  facwordi  13071  faclbnd4lem4  13078  bccl  13104  hashnfinnn0  13147  hashgt12el  13205  hashgt12el2  13206  hashfun  13219  hashbclem  13231  hashbc  13232  hashfacen  13233  hashf1lem1  13234  hashf1  13236  hash2pwpr  13253  fundmge2nop0  13269  fi1uzind  13274  brfi1indALT  13277  fi1uzindOLD  13280  brfi1indALTOLD  13283  wrdind  13470  wrd2ind  13471  reuccats1  13474  swrdccatin1  13477  swrdccatin2  13481  swrdccat3  13486  swrdccat3blem  13489  cshw1  13562  cshwcsh2id  13568  wwlktovfo  13695  s3iunsndisj  13701  rtrclreclem3  13794  dfrtrcl2  13796  sqrlem1  13977  sqrlem6  13982  rexanre  14080  cau3lem  14088  2clim  14297  summo  14442  fsum2dlem  14495  fsumiun  14547  prodmo  14660  fprod2dlem  14704  bpolycl  14777  rpnnen2lem12  14948  odd2np1lem  15058  oddge22np1  15067  sqoddm1div8z  15072  sumeven  15104  pwp1fsum  15108  bitsfzo  15151  sadcaddlem  15173  gcd0id  15234  algcvgblem  15284  lcmfunsnlem1  15344  lcmfunsnlem2lem1  15345  lcmfunsnlem2  15347  coprmproddvdslem  15370  divgcdcoprm0  15373  isprm7  15414  prmdvdsexpr  15423  prmfac1  15425  qnumdencl  15441  hashdvds  15474  prm23lt5  15513  pcneg  15572  prmpwdvds  15602  prmreclem2  15615  4sqlem12  15654  vdwlem6  15684  vdwlem10  15688  vdwlem13  15691  0ram  15718  ram0  15720  ramz  15723  ramcl  15727  prmgaplem3  15751  prmgaplem4  15752  prmgaplem5  15753  prmgaplem6  15754  cshwshashlem1  15796  prmlem0  15806  firest  16087  imasaddfnlem  16182  imasvscafn  16191  mremre  16258  cicsym  16458  initoid  16649  termoid  16650  iszeroi  16653  drsdirfi  16932  pospo  16967  joinfval  16995  meetfval  17009  lubun  17117  odupos  17129  acsfiindd  17171  psss  17208  mnd1id  17326  dfgrp2e  17442  dfgrp3lem  17507  symgfix2  17830  f1omvdco2  17862  symggen  17884  odcau  18013  pgpfi  18014  sylow2blem3  18031  sylow3lem2  18037  lsmmod  18082  efgsfo  18146  frgpuptinv  18178  frgpnabllem1  18270  cyggeninv  18279  lt6abl  18290  cyggex2  18292  gsumval3lem2  18301  gsumval3  18302  gsum2d2  18367  dmdprdd  18392  dprd2da  18435  pgpfac1lem5  18472  pgpfac  18477  srgbinomlem4  18537  dvdsrtr  18646  dvdsrmul1  18647  lss1d  18957  lspsolvlem  19136  lspsnat  19139  lbsextlem2  19153  lbsextlem3  19154  0ring  19264  01eq0ring  19266  0ring01eqbi  19267  rng1nfld  19272  domnmuln0  19292  abvn0b  19296  mvrf1  19419  mplcoe5lem  19461  opsrtoslem2  19479  cply1mul  19658  coe1fzgsumdlem  19665  gsummoncoe1  19668  pf1ind  19713  evl1gsumdlem  19714  xrsdsreclblem  19786  qsssubdrg  19799  prmirredlem  19835  cygznlem3  19912  obslbs  20068  dsmmacl  20079  lindfrn  20154  lmiclbs  20170  lmisfree  20175  matecl  20225  mat1dimelbas  20271  scmateALT  20312  mdetdiaglem  20398  mdet0  20406  mdetunilem9  20420  gsummatr01  20459  cpmatmcllem  20517  m2cpminvid2lem  20553  pmatcollpw3fi1lem2  20586  chfacfscmul0  20657  chfacfpmmul0  20661  cayhamlem3  20686  tgcl  20767  tgidm  20778  indistopon  20799  fctop  20802  cctop  20804  ppttop  20805  pptbas  20806  epttop  20807  opnnei  20918  neiptopnei  20930  tgrest  20957  restntr  20980  perfopn  20983  ordtrest2lem  21001  isreg2  21175  lmmo  21178  ordthauslem  21181  cmpsublem  21196  cmpsub  21197  cmpcld  21199  hauscmplem  21203  iunconnlem  21224  unconn  21226  2ndcrest  21251  2ndcctbss  21252  2ndcdisj  21253  dis2ndc  21257  locfincmp  21323  comppfsc  21329  txbas  21364  ptbasin  21374  ptbasfi  21378  txcls  21401  txbasval  21403  ptpjopn  21409  ptclsg  21412  dfac14lem  21414  xkoccn  21416  txcnp  21417  txindis  21431  txdis1cn  21432  tx1stc  21447  tx2ndc  21448  txkgen  21449  xkoco1cn  21454  xkoco2cn  21455  xkococn  21457  xkoinjcn  21484  txconn  21486  fbfinnfr  21639  opnfbas  21640  filtop  21653  isfild  21656  fbunfip  21667  filconn  21681  fbasrn  21682  filuni  21683  isufil2  21706  filssufilg  21709  ufileu  21717  filufint  21718  rnelfmlem  21750  rnelfm  21751  fmfnfmlem2  21753  fmfnfmlem4  21755  fmfnfm  21756  hausflimi  21778  hauspwpwf1  21785  flffbas  21793  flftg  21794  alexsublem  21842  alexsubALTlem1  21845  alexsubALTlem2  21846  alexsubALTlem3  21847  alexsubALTlem4  21848  alexsubALT  21849  ptcmplem3  21852  cldsubg  21908  qustgpopn  21917  tgptsmscld  21948  tsmsxplem1  21950  ustfilxp  22010  imasdsf1olem  22172  bldisj  22197  xbln0  22213  prdsxmslem2  22328  xrsblre  22608  icccmplem2  22620  reconn  22625  opnreen  22628  xrge0tsms  22631  metdsre  22650  iccpnfcnv  22737  cnheiborlem  22747  phtpc01  22790  pi1blem  22833  tchcph  23030  cfilfcls  23066  iscau4  23071  bcthlem5  23119  bcth3  23122  hlhil  23208  ovolctb  23252  ovoliunlem2  23265  ovoliunnul  23269  ovolicc2  23284  volfiniun  23309  iundisj  23310  dyadmax  23360  dyadmbllem  23361  vitalilem2  23372  ismbfd  23401  mbfimaopnlem  23416  itg11  23452  i1faddlem  23454  mbfi1fseqlem4  23479  bddmulibl  23599  limciun  23652  perfdvf  23661  rolle  23747  dvivthlem1  23765  dvne0  23768  lhop1  23771  lhop2  23772  itgsubst  23806  dvdsq1p  23914  fta1g  23921  dgrco  24025  plydivex  24046  fta1  24057  ulmcaulem  24142  abelthlem2  24180  pilem2  24200  cxpmul2z  24431  cxpcn3lem  24482  xrlimcnp  24689  jensen  24709  wilthlem2  24789  wilthlem3  24790  muval2  24854  sqf11  24859  ppiublem1  24921  fsumvma  24932  lgsdir2lem2  25045  lgsdir2lem5  25048  lgsqrmodndvds  25072  gausslemma2dlem1a  25084  gausslemma2dlem3  25087  gausslemma2d  25093  2lgsoddprmlem2  25128  dchrisum0fno1  25194  pntlem3  25292  pntleml  25294  ostthlem1  25310  ostth2lem2  25317  colinearalg  25784  axcontlem2  25839  axcontlem8  25845  edgupgr  26023  umgrpredgv  26029  numedglnl  26033  ausgrumgri  26056  ausgrusgri  26057  ushgredgedg  26115  ushgredgedgloop  26117  uhgr0v0e  26124  subumgredg2  26171  uhgrspansubgrlem  26176  uhgrspan1  26189  upgrreslem  26190  umgrreslem  26191  upgrres1  26199  fusgrfisstep  26215  nbuhgr  26233  nbuhgr2vtx1edgb  26242  uhgrnbgr0nb  26244  edgnbusgreu  26263  nbusgredgeu0  26264  nbusgrf1o0  26265  nbusgrvtxm1uvtx  26300  cusgredg  26314  cusgrfi  26348  usgredgsscusgredg  26349  1loopgrnb0  26392  usgrvd0nedg  26423  uhgrvd00  26424  upgriswlk  26531  upgrwlkcompim  26533  uspgr2wlkeq  26536  uspgr2wlkeqi  26538  wlkv0  26541  wlklenvclwlk  26545  wlkp1lem6  26569  lfgrwlkprop  26578  spthdep  26624  upgrwlkdvdelem  26626  usgr2wlkneq  26646  usgr2trlncl  26650  pthdlem1  26656  pthdlem2lem  26657  clwlkl1loop  26672  crctcshwlkn0lem3  26698  crctcshwlkn0lem5  26700  crctcshwlkn0  26707  0enwwlksnge1  26743  wlkiswwlks2  26755  wlkiswwlksupgr2  26757  wlkwwlksur  26777  umgr2adedgspth  26838  wwlks2onv  26841  clwlkclwwlklem2a4  26892  clwlkclwwlklem2  26895  clwwlksf1  26910  erclwwlkstr  26929  erclwwlksntr  26941  hashecclwwlksn1  26947  umgrhashecclwwlk  26948  clwlksfoclwwlk  26956  eucrctshift  27096  3cyclfrgrrn1  27142  frgrnbnb  27150  frgrncvvdeqlem2  27157  frgrncvvdeqlem3  27158  frgrncvvdeqlem9  27164  frgrwopreglem5  27171  frgrwopreg1  27173  frgrwopreg2  27174  numclwwlkovf2ex  27204  numclwlk1lem2f1  27211  lnon0  27637  shmodsi  28232  shlub  28257  spanunsni  28422  h1datomi  28424  stm1ri  29087  stadd3i  29091  mdsl1i  29164  cvmdi  29167  superpos  29197  chjatom  29200  chirredi  29237  atcvat4i  29240  sumdmdii  29258  sumdmdlem  29261  cdj3lem2a  29279  cdj3lem3a  29282  cdj3i  29284  disji2f  29374  disjif2  29378  iundisjf  29386  rnmpt2ss  29458  iundisjfi  29540  nn0min  29552  xrge0tsmsd  29770  cnre2csqima  29942  ordtrest2NEWlem  29953  xrge0iifcnv  29964  lmxrge0  29983  measdivcstOLD  30272  dya2iocuni  30330  omssubadd  30347  eulerpartlems  30407  bnj849  30980  bnj1118  31037  derangenlem  31138  erdszelem9  31166  pconnconn  31198  iccllysconn  31217  cvmsval  31233  cvmscld  31240  cvmsss2  31241  cvmopnlem  31245  cvmfolem  31246  cvmliftmolem2  31249  cvmlift2lem10  31279  cvmlift2lem12  31281  cvmlift3lem5  31290  cvmlift3lem8  31293  msubvrs  31442  mthmblem  31462  untsucf  31572  3orel1  31577  3orel2  31578  3orel3  31579  nepss  31585  eqfunresadj  31645  dfon2lem5  31676  dfon2lem6  31677  dfon2lem7  31678  dfon2lem8  31679  rdgprc  31684  trpredtr  31714  dftrpred3g  31717  trpredrec  31722  frmin  31723  frind  31724  frins2fg  31728  wzel  31755  wsuclem  31757  wsuclemOLD  31758  frrlem5e  31772  nosepon  31802  noextendseq  31804  nolesgn2ores  31809  nosepdmlem  31817  nodenselem8  31825  noetalem3  31849  nocvxmin  31878  scutun12  31901  funpartfun  32034  altopth1  32056  altopth2  32057  colineardim1  32152  lineext  32167  btwnconn1lem14  32191  brsegle  32199  hilbert1.2  32246  trer  32294  elicc3  32295  finminlem  32296  fneint  32327  fnessref  32336  refssfne  32337  neibastop1  32338  neibastop2lem  32339  neibastop2  32340  fnemeet2  32346  fnejoin2  32348  tailfb  32356  arg-ax  32399  ordtoplem  32418  onsuct0  32424  bj-gl4lem  32563  bj-sngltag  32955  bj-restn0  33027  bj-0int  33039  bj-ismooredr2  33049  bj-bary1lem1  33141  icorempt2  33179  icoreresf  33180  relowlssretop  33191  finxpreclem6  33213  wl-ax8clv2  33361  fin2so  33376  poimirlem24  33413  poimirlem25  33414  poimirlem26  33415  poimirlem27  33416  poimirlem29  33418  poimirlem30  33419  poimirlem31  33420  mblfinlem1  33426  mblfinlem4  33429  ovoliunnfl  33431  itg2addnclem  33441  itg2addnclem2  33442  areacirc  33485  unirep  33487  filbcmb  33515  sdclem1  33519  fdc  33521  nninfnub  33527  isbnd2  33562  ssbnd  33567  prdsbnd2  33574  cntotbnd  33575  heibor1lem  33588  heiborlem1  33590  heiborlem4  33593  heiborlem6  33595  0idl  33804  intidl  33808  unichnidl  33810  keridl  33811  prnc  33846  prtlem17  33987  prter2  33992  ax12indn  34054  lsatn0  34112  lsatcmp  34116  lssat  34129  lfl1  34183  lshpsmreu  34222  lkrin  34277  glbconxN  34490  cvrat4  34555  paddasslem17  34948  pmodlem2  34959  dalawlem14  34996  pclclN  35003  pclfinN  35012  pclfinclN  35062  poml4N  35065  osumcllem8N  35075  pexmidlem5N  35086  cdleme32a  35555  cdlemg33b0  35815  tendoeq2  35888  diaelrnN  36160  dihmeetlem1N  36405  dihglblem5apreN  36406  dihglblem2N  36409  dochvalr  36472  dochkrshp  36501  lcfl6  36615  lcfrvalsnN  36656  mapdordlem2  36752  mapdh8b  36895  mapdh9a  36905  hdmap14lem13  36998  eldioph2b  37152  eldiophss  37164  diophren  37203  ctbnfien  37208  rencldnfilem  37210  pellexlem3  37221  pellexlem5  37223  pellex  37225  pell14qrexpcl  37257  pellfundre  37271  pellfundge  37272  pellfundlb  37274  pellfundglb  37275  jm2.19lem4  37385  fnwe2lem2  37447  pwssplit4  37485  hbtlem5  37524  ss2iundf  37777  relexpmulg  37828  relexpxpmin  37835  relexpaddss  37836  dftrcl3  37838  dfrtrcl3  37851  clsk1indlem3  38167  isotone1  38172  isotone2  38173  ntrneiel2  38210  ntrneik4w  38224  onfrALT  38590  ax6e2ndeq  38601  snssiALT  38889  iinssf  39153  hirstL-ax3  40828  2reurex  40950  otiunsndisjX  41067  subsubelfzo0  41105  iccpartiltu  41128  iccpartigtl  41129  iccpartltu  41131  pfxccat3  41197  pfxccat3a  41200  reuccatpfxs1  41205  fmtnofac2lem  41251  fmtno4prmfac  41255  prmdvdsfmtnof1lem1  41267  lighneallem2  41294  opoeALTV  41365  opeoALTV  41366  even3prm2  41399  gbegt5  41420  gbowgt5  41421  sbgoldbwt  41436  sbgoldbst  41437  sbgoldbalt  41440  sbgoldbm  41443  mogoldbb  41444  sbgoldbo  41446  nnsum3primesle9  41453  nnsum4primeseven  41459  nnsum4primesevenALTV  41460  wtgoldbnnsum4prm  41461  bgoldbnnsum3prm  41463  bgoldbtbndlem1  41464  bgoldbtbndlem4  41467  bgoldbtbnd  41468  upgrwlkupwlk  41492  sprsymrelf1lem  41512  sprsymrelfolem2  41514  sprsymrelf1  41517  sprsymrelfo  41518  mgmpropd  41546  copisnmnd  41580  mgm2mgm  41634  ringrng  41650  c0snmgmhm  41685  ztprmneprm  41896  mndpsuppss  41923  lindslinindimp2lem4  42021  lindslinindsimp2  42023  lindsrng01  42028  snlindsntor  42031  ldepspr  42033  isldepslvec2  42045  suppdm  42071  blen1b  42153  dignn0ldlem  42167  digexp  42172  nn0sumshdiglemB  42185  nn0sumshdiglem1  42186  iunord  42193  tfis2d  42198
  Copyright terms: Public domain W3C validator