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  469  3orel1  1076  3jao  1526  nfimdOLDOLD  1961  axc16nf  2272  ax13  2382  2euex  2670  2eu1  2679  eqneqall  2931  necon3bd  2934  pm2.61dne  3006  elnelall  3036  spcimgft  3412  rspc  3431  rspcimdv  3438  rspc2gv  3448  euind  3522  reuind  3540  sbciegft  3595  rspsbc  3647  ssexnelpss  3850  ralnralall  4212  pwpw0  4477  sssn  4491  eqsnOLD  4495  prel12OLD  4515  prnebg  4521  pwsnALT  4569  intss1  4632  intmin  4637  uniintsn  4654  iinss  4711  iinss2  4712  disji2  4776  disjiun  4780  disjiund  4783  disjxiun  4789  trel3  4900  trin  4903  trintssOLD  4910  eusvnfb  4999  reusv3  5013  copsexg  5092  propeqop  5106  otiunsndisj  5118  iunopeqop  5119  po3nr  5189  fri  5216  wefrc  5248  wereu2  5251  ssrelrel  5365  relop  5416  iss  5593  restidsingOLD  5605  poirr2  5666  xpcan  5716  xpcan2  5717  sossfld  5726  wfi  5862  wfis2fg  5866  onfr  5912  onmindif  5964  funopg  6071  funssres  6079  funun  6081  fv3  6355  fvmptt  6450  iinpreima  6496  fvn0ssdmfun  6501  dff3  6523  dff4  6524  fmptsng  6586  fmptsnd  6587  tpres  6618  fnprb  6624  fntpb  6625  fvclss  6651  fpropnf1  6675  isomin  6738  isofrlem  6741  weniso  6755  oprabid  6828  ssorduni  7138  onmindif2  7165  limuni3  7205  tfis2f  7208  tfinds  7212  tfinds2  7216  tfinds3  7217  funcnvuni  7272  f1oweALT  7305  f1o2ndf1  7441  poxp  7445  soxp  7446  fnse  7450  suppimacnv  7462  mpt2xopynvov0g  7497  reldmtpos  7517  rntpos  7522  wfrlem14  7585  wfrlem15  7586  onfununi  7595  smoiun  7615  tfrlem1  7629  tfr3  7652  frsucmptn  7691  tz7.49  7697  oaordi  7783  oawordeulem  7791  omeulem1  7819  oeordi  7824  oelimcl  7837  nnaordi  7855  nneob  7889  omsmolem  7890  erdisj  7949  qsss  7963  uniinqs  7982  map0g  8051  resixpfo  8100  ixpsnf1o  8102  xpdom3  8211  mapdom3  8285  phplem4  8295  php3  8299  unxpdomlem3  8319  ssfi  8333  findcard2  8353  findcard3  8356  frfi  8358  isfiniteg  8373  xpfi  8384  fiint  8390  finsschain  8426  dffi2  8482  marypha1lem  8492  marypha2  8498  supmo  8511  suplub2  8520  infmo  8554  ordiso2  8573  ordtypelem7  8582  ordtypelem8  8583  brwdom2  8631  unxpwdom2  8646  ixpiunwdom  8649  elirrv  8654  suc11reg  8677  noinfep  8718  cantnfle  8729  cantnflem1  8747  cantnf  8751  trcl  8765  epfrs  8768  rankpwi  8847  rankunb  8874  rankuni2b  8877  rankxplim3  8905  cplem1  8913  karden  8919  carddom2  8964  fseqenlem2  9009  ac10ct  9018  acni2  9030  acndom  9035  infpwfien  9046  alephordi  9058  alephord  9059  iunfictbso  9098  aceq3lem  9104  dfac5  9112  dfac2b  9114  dfac2OLD  9116  dfac12lem3  9130  dfac12r  9131  cdainflem  9176  cdainf  9177  cfub  9234  cfeq0  9241  coflim  9246  cfslb2n  9253  cofsmo  9254  coftr  9258  infpssr  9293  fin23lem7  9301  fin23lem11  9302  fin23lem21  9324  isf32lem2  9339  isf34lem4  9362  isfin1-2  9370  isfin1-3  9371  fin1a2lem9  9393  fin1a2lem11  9395  fin1a2lem12  9396  fin1a2lem13  9397  domtriomlem  9427  axdc3lem2  9436  axcclem  9442  ac6c4  9466  zorn2lem4  9484  zorn2lem5  9485  zorn2lem7  9487  ttukeylem5  9498  ttukeyg  9502  brdom6disj  9517  fnrndomg  9521  iunfo  9524  iundom2g  9525  ficard  9550  konigthlem  9553  alephval2  9557  pwcfsdom  9568  fpwwe2lem9  9623  fpwwe2lem11  9625  fpwwe2lem12  9626  fpwwe2lem13  9627  pwfseqlem3  9645  gchpwdom  9655  winalim2  9681  gchina  9684  wunex2  9723  tskr1om2  9753  tskxpss  9757  inar1  9760  tskuni  9768  gruun  9791  grudomon  9802  grur1  9805  ltmpi  9889  ltexprlem2  10022  ltexprlem6  10026  reclem2pr  10033  reclem3pr  10034  reclem4pr  10035  suplem1pr  10037  mulgt0sr  10089  supsrlem  10095  axrrecex  10147  axpre-sup  10153  ltlen  10301  addid0  10613  negn0  10622  negf1o  10623  mulge0b  11056  supaddc  11153  supadd  11154  supmul1  11155  supmullem1  11156  supmullem2  11157  supmul  11158  cju  11179  nnsub  11222  0mnnnnn0  11488  un0addcl  11489  un0mulcl  11490  nn0sub  11506  nn0n0n1ge2b  11522  peano5uzi  11629  eluzuzle  11859  zsupss  11941  qbtwnre  12194  xrsupexmnf  12299  xrinfmexpnf  12300  xrsupsslem  12301  xrinfmsslem  12302  xrub  12306  supxrun  12310  ixxdisj  12354  icodisj  12461  difreicc  12468  uzsubsubfz  12527  fzadd2  12540  elfzmlbp  12615  fzofzim  12680  elfznelfzo  12738  injresinj  12754  subfzo0  12755  flval3  12781  modirr  12906  modsumfzodifsn  12908  addmodlteq  12910  ssnn0fi  12949  seqf1o  13007  expcl2lem  13037  expnegz  13059  expaddz  13069  expmulz  13071  facwordi  13241  faclbnd4lem4  13248  bccl  13274  hashnfinnn0  13315  hashgt12el  13373  hashgt12el2  13374  hashfun  13387  hashbclem  13399  hashbc  13400  hashfacen  13401  hashf1lem1  13402  hashf1  13404  hash2pwpr  13421  fundmge2nop0  13437  fi1uzind  13442  brfi1indALT  13445  wrdind  13647  wrd2ind  13648  reuccats1  13651  swrdccatin1  13654  swrdccatin2  13658  swrdccat3  13663  swrdccat3blem  13666  cshw1  13739  cshwcsh2id  13745  wwlktovfo  13873  s3iunsndisj  13879  rtrclreclem3  13970  dfrtrcl2  13972  sqrlem1  14153  sqrlem6  14158  rexanre  14256  cau3lem  14264  2clim  14473  summo  14618  fsum2dlem  14671  fsumiun  14723  prodmo  14836  fprod2dlem  14880  bpolycl  14953  rpnnen2lem12  15124  odd2np1lem  15237  oddge22np1  15246  sqoddm1div8z  15251  sumeven  15283  pwp1fsum  15287  bitsfzo  15330  sadcaddlem  15352  gcd0id  15413  algcvgblem  15463  lcmfunsnlem1  15523  lcmfunsnlem2lem1  15524  lcmfunsnlem2  15526  coprmproddvdslem  15549  divgcdcoprm0  15552  isprm7  15593  prmdvdsexpr  15602  prmfac1  15604  qnumdencl  15620  hashdvds  15653  prm23lt5  15692  pcneg  15751  prmpwdvds  15781  prmreclem2  15794  4sqlem12  15833  vdwlem6  15863  vdwlem10  15867  vdwlem13  15870  0ram  15897  ram0  15899  ramz  15902  ramcl  15906  prmgaplem3  15930  prmgaplem4  15931  prmgaplem5  15932  prmgaplem6  15933  cshwshashlem1  15975  prmlem0  15985  firest  16266  imasaddfnlem  16361  imasvscafn  16370  mremre  16437  cicsym  16636  initoid  16827  termoid  16828  iszeroi  16831  drsdirfi  17110  pospo  17145  joinfval  17173  meetfval  17187  lubun  17295  odupos  17307  acsfiindd  17349  psss  17386  mnd1id  17504  dfgrp2e  17620  dfgrp3lem  17685  symgfix2  18007  f1omvdco2  18039  symggen  18061  odcau  18190  pgpfi  18191  sylow2blem3  18208  sylow3lem2  18214  lsmmod  18259  efgsfo  18323  frgpuptinv  18355  frgpnabllem1  18447  cyggeninv  18456  lt6abl  18467  cyggex2  18469  gsumval3lem2  18478  gsumval3  18479  gsum2d2  18544  dmdprdd  18569  dprd2da  18612  pgpfac1lem5  18649  pgpfac  18654  srgbinomlem4  18714  dvdsrtr  18823  dvdsrmul1  18824  lss1d  19136  lspsolvlem  19315  lspsnat  19318  lbsextlem2  19332  lbsextlem3  19333  0ring  19443  01eq0ring  19445  0ring01eqbi  19446  rng1nfld  19451  domnmuln0  19471  abvn0b  19475  mvrf1  19598  mplcoe5lem  19640  opsrtoslem2  19658  cply1mul  19837  coe1fzgsumdlem  19844  gsummoncoe1  19847  pf1ind  19892  evl1gsumdlem  19893  xrsdsreclblem  19965  qsssubdrg  19978  prmirredlem  20014  cygznlem3  20091  obslbs  20247  dsmmacl  20258  lindfrn  20333  lmiclbs  20349  lmisfree  20354  matecl  20404  mat1dimelbas  20450  scmateALT  20491  mdetdiaglem  20577  mdet0  20585  mdetunilem9  20599  gsummatr01  20638  cpmatmcllem  20696  m2cpminvid2lem  20732  pmatcollpw3fi1lem2  20765  chfacfscmul0  20836  chfacfpmmul0  20840  cayhamlem3  20865  tgcl  20946  tgidm  20957  indistopon  20978  fctop  20981  cctop  20983  ppttop  20984  pptbas  20985  epttop  20986  opnnei  21097  neiptopnei  21109  tgrest  21136  restntr  21159  perfopn  21162  ordtrest2lem  21180  isreg2  21354  lmmo  21357  ordthauslem  21360  cmpsublem  21375  cmpsub  21376  cmpcld  21378  hauscmplem  21382  iunconnlem  21403  unconn  21405  2ndcrest  21430  2ndcctbss  21431  2ndcdisj  21432  dis2ndc  21436  locfincmp  21502  comppfsc  21508  txbas  21543  ptbasin  21553  ptbasfi  21557  txcls  21580  txbasval  21582  ptpjopn  21588  ptclsg  21591  dfac14lem  21593  xkoccn  21595  txcnp  21596  txindis  21610  txdis1cn  21611  tx1stc  21626  tx2ndc  21627  txkgen  21628  xkoco1cn  21633  xkoco2cn  21634  xkococn  21636  xkoinjcn  21663  txconn  21665  fbfinnfr  21817  opnfbas  21818  filtop  21831  isfild  21834  fbunfip  21845  filconn  21859  fbasrn  21860  filuni  21861  isufil2  21884  filssufilg  21887  ufileu  21895  filufint  21896  rnelfmlem  21928  rnelfm  21929  fmfnfmlem2  21931  fmfnfmlem4  21933  fmfnfm  21934  hausflimi  21956  hauspwpwf1  21963  flffbas  21971  flftg  21972  alexsublem  22020  alexsubALTlem1  22023  alexsubALTlem2  22024  alexsubALTlem3  22025  alexsubALTlem4  22026  alexsubALT  22027  ptcmplem3  22030  cldsubg  22086  qustgpopn  22095  tgptsmscld  22126  tsmsxplem1  22128  ustfilxp  22188  imasdsf1olem  22350  bldisj  22375  xbln0  22391  prdsxmslem2  22506  xrsblre  22786  icccmplem2  22798  reconn  22803  opnreen  22806  xrge0tsms  22809  metdsre  22828  iccpnfcnv  22915  cnheiborlem  22925  phtpc01  22967  pi1blem  23010  tchcph  23207  cfilfcls  23243  iscau4  23248  bcthlem5  23296  bcth3  23299  hlhil  23385  ovolctb  23429  ovoliunlem2  23442  ovoliunnul  23446  ovolicc2  23461  volfiniun  23486  iundisj  23487  dyadmax  23537  dyadmbllem  23538  vitalilem2  23548  ismbfd  23577  mbfimaopnlem  23592  itg11  23628  i1faddlem  23630  mbfi1fseqlem4  23655  bddmulibl  23775  limciun  23828  perfdvf  23837  rolle  23923  dvivthlem1  23941  dvne0  23944  lhop1  23947  lhop2  23948  itgsubst  23982  dvdsq1p  24090  fta1g  24097  dgrco  24201  plydivex  24222  fta1  24233  ulmcaulem  24318  abelthlem2  24356  pilem2  24376  cxpmul2z  24607  cxpcn3lem  24658  xrlimcnp  24865  jensen  24885  wilthlem2  24965  wilthlem3  24966  muval2  25030  sqf11  25035  ppiublem1  25097  fsumvma  25108  lgsdir2lem2  25221  lgsdir2lem5  25224  lgsqrmodndvds  25248  gausslemma2dlem1a  25260  gausslemma2dlem3  25263  gausslemma2d  25269  2lgsoddprmlem2  25304  dchrisum0fno1  25370  pntlem3  25468  pntleml  25470  ostthlem1  25486  ostth2lem2  25493  colinearalg  25960  axcontlem2  26015  axcontlem8  26021  edgupgr  26199  umgrpredgv  26205  numedglnl  26209  ausgrumgri  26232  ausgrusgri  26233  ushgredgedg  26291  ushgredgedgloop  26293  uhgr0v0e  26300  subumgredg2  26347  uhgrspansubgrlem  26352  uhgrspan1  26365  upgrreslem  26366  umgrreslem  26367  upgrres1  26375  fusgrfisstep  26391  nbuhgr  26409  nbuhgr2vtx1edgblem  26417  nbuhgr2vtx1edgb  26418  uhgrnbgr0nb  26420  edgnbusgreu  26438  nbusgredgeu0  26439  nbusgrf1o0  26440  nbusgrvtxm1uvtx  26481  cusgredg  26501  cusgrfi  26535  usgredgsscusgredg  26536  1loopgrnb0  26579  usgrvd0nedg  26610  uhgrvd00  26611  upgriswlk  26718  upgrwlkcompim  26720  uspgr2wlkeq  26723  uspgr2wlkeqi  26725  wlkv0  26728  wlklenvclwlk  26732  wlkp1lem6  26756  lfgrwlkprop  26765  spthdep  26811  upgrwlkdvdelem  26813  usgr2wlkneq  26833  usgr2trlncl  26837  pthdlem1  26843  pthdlem2lem  26844  clwlkl1loop  26860  crctcshwlkn0lem3  26886  crctcshwlkn0lem5  26888  crctcshwlkn0  26895  0enwwlksnge1  26944  wlkiswwlks2  26955  wlkiswwlksupgr2  26957  wlkwwlksur  26977  wspthsnonn0vne  27008  umgr2adedgspth  27039  clwlkclwwlklem2a4  27091  clwlkclwwlklem2  27094  clwlkclwwlkf  27102  clwlkclwwlkfo  27103  erclwwlktr  27116  clwwlkf1  27149  erclwwlkntr  27173  hashecclwwlkn1  27179  umgrhashecclwwlk  27180  clwlksfoclwwlkOLD  27188  clwwlknonex2e  27230  eucrctshift  27366  3cyclfrgrrn1  27410  frgrnbnb  27418  frgrncvvdeqlem2  27425  frgrncvvdeqlem3  27426  frgrncvvdeqlem9  27432  frgrwopreglem4a  27435  frgrwopregbsn  27442  frgrwopreg1  27443  frgrwopreg2  27444  frgrwopreglem5lem  27445  frgrwopreglem5ALT  27447  frgr2wwlk1  27454  numclwlk1lem2foa  27484  numclwlk1lem2f1  27487  wlkl0  27499  lnon0  27933  shmodsi  28528  shlub  28553  spanunsni  28718  h1datomi  28720  stm1ri  29383  stadd3i  29387  mdsl1i  29460  cvmdi  29463  superpos  29493  chjatom  29496  chirredi  29533  atcvat4i  29536  sumdmdii  29554  sumdmdlem  29557  cdj3lem2a  29575  cdj3lem3a  29578  cdj3i  29580  disji2f  29668  disjif2  29672  iundisjf  29680  rnmpt2ss  29753  iundisjfi  29835  nn0min  29847  xrge0tsmsd  30065  cnre2csqima  30237  ordtrest2NEWlem  30248  xrge0iifcnv  30259  lmxrge0  30278  measdivcstOLD  30567  dya2iocuni  30625  omssubadd  30642  eulerpartlems  30702  bnj849  31273  bnj1118  31330  derangenlem  31431  erdszelem9  31459  pconnconn  31491  iccllysconn  31510  cvmsval  31526  cvmscld  31533  cvmsss2  31534  cvmopnlem  31538  cvmfolem  31539  cvmliftmolem2  31542  cvmlift2lem10  31572  cvmlift2lem12  31574  cvmlift3lem5  31583  cvmlift3lem8  31586  msubvrs  31735  mthmblem  31755  untsucf  31865  3orel2  31870  3orel3  31871  nepss  31877  eqfunresadj  31937  dfon2lem5  31968  dfon2lem6  31969  dfon2lem7  31970  dfon2lem8  31971  rdgprc  31976  trpredtr  32006  dftrpred3g  32009  trpredrec  32014  frpomin  32015  frpoind  32017  frmin  32019  frind  32020  frins2fg  32024  wzel  32046  wsuclem  32047  frrlem5e  32065  nosepon  32095  noextendseq  32097  nolesgn2ores  32102  nosepdmlem  32110  nodenselem8  32118  noetalem3  32142  nocvxmin  32171  scutun12  32194  funpartfun  32327  altopth1  32349  altopth2  32350  colineardim1  32445  lineext  32460  btwnconn1lem14  32484  brsegle  32492  hilbert1.2  32539  trer  32587  elicc3  32588  finminlem  32589  fneint  32620  fnessref  32629  refssfne  32630  neibastop1  32631  neibastop2lem  32632  neibastop2  32633  fnemeet2  32639  fnejoin2  32641  tailfb  32649  arg-ax  32692  ordtoplem  32711  onsuct0  32717  bj-gl4lem  32856  bj-sngltag  33248  bj-restn0  33320  bj-0int  33332  bj-ismooredr2  33342  bj-bary1lem1  33443  icorempt2  33481  icoreresf  33482  relowlssretop  33493  finxpreclem6  33515  wl-ax8clv2  33663  fin2so  33678  poimirlem24  33715  poimirlem25  33716  poimirlem26  33717  poimirlem27  33718  poimirlem29  33720  poimirlem30  33721  poimirlem31  33722  mblfinlem1  33728  mblfinlem4  33731  ovoliunnfl  33733  itg2addnclem  33743  itg2addnclem2  33744  areacirc  33787  unirep  33789  filbcmb  33817  sdclem1  33821  fdc  33823  nninfnub  33829  isbnd2  33864  ssbnd  33869  prdsbnd2  33876  cntotbnd  33877  heibor1lem  33890  heiborlem1  33892  heiborlem4  33895  heiborlem6  33897  0idl  34106  intidl  34110  unichnidl  34112  keridl  34113  prnc  34148  iss2  34404  prtlem17  34634  prter2  34639  ax12indn  34701  lsatn0  34758  lsatcmp  34762  lssat  34775  lfl1  34829  lshpsmreu  34868  lkrin  34923  glbconxN  35136  cvrat4  35201  paddasslem17  35594  pmodlem2  35605  dalawlem14  35642  pclclN  35649  pclfinN  35658  pclfinclN  35708  poml4N  35711  osumcllem8N  35721  pexmidlem5N  35732  cdleme32a  36200  cdlemg33b0  36460  tendoeq2  36533  diaelrnN  36805  dihmeetlem1N  37050  dihglblem5apreN  37051  dihglblem2N  37054  dochvalr  37117  dochkrshp  37146  lcfl6  37260  lcfrvalsnN  37301  mapdordlem2  37397  mapdh8b  37540  mapdh9a  37550  hdmap14lem13  37643  eldioph2b  37797  eldiophss  37809  diophren  37848  ctbnfien  37853  rencldnfilem  37855  pellexlem3  37866  pellexlem5  37868  pellex  37870  pell14qrexpcl  37902  pellfundre  37916  pellfundge  37917  pellfundlb  37919  pellfundglb  37920  jm2.19lem4  38030  fnwe2lem2  38092  pwssplit4  38130  hbtlem5  38169  ss2iundf  38422  relexpmulg  38473  relexpxpmin  38480  relexpaddss  38481  dftrcl3  38483  dfrtrcl3  38496  clsk1indlem3  38812  isotone1  38817  isotone2  38818  ntrneiel2  38855  ntrneik4w  38869  onfrALT  39235  ax6e2ndeq  39246  snssiALT  39531  iinssf  39795  hirstL-ax3  41534  2reurex  41656  otiunsndisjX  41775  subsubelfzo0  41815  iccpartiltu  41837  iccpartigtl  41838  iccpartltu  41840  pfxccat3  41905  pfxccat3a  41908  reuccatpfxs1  41913  fmtnofac2lem  41959  fmtno4prmfac  41963  prmdvdsfmtnof1lem1  41975  lighneallem2  42002  opoeALTV  42073  opeoALTV  42074  even3prm2  42107  gbegt5  42128  gbowgt5  42129  sbgoldbwt  42144  sbgoldbst  42145  sbgoldbalt  42148  sbgoldbm  42151  mogoldbb  42152  sbgoldbo  42154  nnsum3primesle9  42161  nnsum4primeseven  42167  nnsum4primesevenALTV  42168  wtgoldbnnsum4prm  42169  bgoldbnnsum3prm  42171  bgoldbtbndlem1  42172  bgoldbtbndlem4  42175  bgoldbtbnd  42176  upgrwlkupwlk  42200  sprsymrelf1lem  42220  sprsymrelfolem2  42222  sprsymrelf1  42225  sprsymrelfo  42226  mgmpropd  42254  copisnmnd  42288  mgm2mgm  42342  ringrng  42358  c0snmgmhm  42393  ztprmneprm  42604  mndpsuppss  42631  lindslinindimp2lem4  42729  lindslinindsimp2  42731  lindsrng01  42736  snlindsntor  42739  ldepspr  42741  isldepslvec2  42753  suppdm  42779  blen1b  42861  dignn0ldlem  42875  digexp  42880  nn0sumshdiglemB  42893  nn0sumshdiglem1  42894  iunord  42901  tfis2d  42906
  Copyright terms: Public domain W3C validator