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

Theorem syl5bi 231
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 205 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 33 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  3imtr4g  284  ancomsd  469  3jao  1381  nfimd  1812  axc16nf  2122  ax13  2237  2euex  2532  2eu1  2541  eqneqall  2793  necon3bd  2796  pm2.61dne  2868  spcimgft  3257  rspc  3276  rspcimdv  3283  euind  3360  reuind  3378  sbciegft  3433  rspsbc  3484  ssexnelpss  3682  pwpw0  4284  sssn  4298  eqsnOLD  4302  prel12  4323  prnebg  4329  pwsnALT  4367  intss1  4427  intmin  4432  uniintsn  4449  iinss  4507  iinss2  4508  disji2  4569  disjiun  4573  disjxiun  4579  disjxiunOLD  4580  trel3  4688  trin  4691  trintss  4697  eusvnfb  4788  reusv3  4802  copsexg  4882  propeqop  4895  otiunsndisj  4905  iunopeqop  4906  po3nr  4973  fri  5000  wefrc  5032  wereu2  5035  ssrelrel  5143  relop  5194  iss  5367  restidsingOLD  5378  poirr2  5439  xpcan  5489  xpcan2  5490  sossfld  5499  wfi  5630  wfis2fg  5634  onfr  5680  onmindif  5732  funopg  5836  funssres  5844  funun  5846  fv3  6116  fvmptt  6208  iinpreima  6253  fvn0ssdmfun  6258  dff3  6280  dff4  6281  fmptsng  6339  fmptsnd  6340  tpres  6371  fnprb  6377  fntpb  6378  fvclss  6404  isomin  6487  isofrlem  6490  weniso  6504  oprabid  6576  ssorduni  6877  onmindif2  6904  limuni3  6944  tfis2f  6947  tfinds  6951  tfinds2  6955  tfinds3  6956  funcnvuni  7012  f1oweALT  7043  f1o2ndf1  7172  poxp  7176  soxp  7177  fnse  7181  suppimacnv  7193  mpt2xopynvov0g  7227  reldmtpos  7247  rntpos  7252  wfrlem14  7315  wfrlem15  7316  onfununi  7325  smoiun  7345  tfrlem1  7359  tfr3  7382  frsucmptn  7421  tz7.49  7427  oaordi  7513  oawordeulem  7521  omeulem1  7549  oeordi  7554  oelimcl  7567  nnaordi  7585  nneob  7619  omsmolem  7620  erdisj  7681  qsss  7695  uniinqs  7714  map0g  7783  resixpfo  7832  ixpsnf1o  7834  xpdom3  7943  mapdom3  8017  phplem4  8027  php3  8031  unxpdomlem3  8051  ssfi  8065  findcard2  8085  findcard3  8088  frfi  8090  isfiniteg  8105  xpfi  8116  fiint  8122  finsschain  8156  dffi2  8212  marypha1lem  8222  marypha2  8228  supmo  8241  suplub2  8250  infmo  8284  ordiso2  8303  ordtypelem7  8312  ordtypelem8  8313  brwdom2  8361  unxpwdom2  8376  ixpiunwdom  8379  elirrv  8387  suc11reg  8399  noinfep  8440  cantnfle  8451  cantnflem1  8469  cantnf  8473  trcl  8487  epfrs  8490  rankpwi  8569  rankunb  8596  rankuni2b  8599  rankxplim3  8627  cplem1  8635  karden  8641  carddom2  8686  fseqenlem2  8731  ac10ct  8740  acni2  8752  acndom  8757  infpwfien  8768  alephordi  8780  alephord  8781  iunfictbso  8820  aceq3lem  8826  dfac5  8834  dfac2  8836  dfac12lem3  8850  dfac12r  8851  cdainflem  8896  cdainf  8897  cfub  8954  cfeq0  8961  coflim  8966  cfslb2n  8973  cofsmo  8974  coftr  8978  infpssr  9013  fin23lem7  9021  fin23lem11  9022  fin23lem21  9044  isf32lem2  9059  isf34lem4  9082  isfin1-2  9090  isfin1-3  9091  fin1a2lem9  9113  fin1a2lem11  9115  fin1a2lem12  9116  fin1a2lem13  9117  domtriomlem  9147  axdc3lem2  9156  axcclem  9162  ac6c4  9186  zorn2lem4  9204  zorn2lem5  9205  zorn2lem7  9207  ttukeylem5  9218  ttukeyg  9222  brdom6disj  9235  fnrndomg  9239  iunfo  9240  iundom2g  9241  ficard  9266  konigthlem  9269  alephval2  9273  pwcfsdom  9284  fpwwe2lem9  9339  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  pwfseqlem3  9361  gchpwdom  9371  winalim2  9397  gchina  9400  wunex2  9439  tskr1om2  9469  tskxpss  9473  inar1  9476  tskuni  9484  gruun  9507  grudomon  9518  grur1  9521  ltmpi  9605  ltexprlem2  9738  ltexprlem6  9742  reclem2pr  9749  reclem3pr  9750  reclem4pr  9751  suplem1pr  9753  mulgt0sr  9805  supsrlem  9811  axrrecex  9863  axpre-sup  9869  ltlen  10017  addid0  10329  negn0  10338  negf1o  10339  mulge0b  10772  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  cju  10893  nnsub  10936  0mnnnnn0  11202  un0addcl  11203  un0mulcl  11204  nn0sub  11220  nn0n0n1ge2b  11236  peano5uzi  11342  eluzuzle  11572  zsupss  11653  qbtwnre  11904  xrsupexmnf  12007  xrinfmexpnf  12008  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrun  12018  ixxdisj  12061  icodisj  12168  difreicc  12175  uzsubsubfz  12234  fzadd2  12247  elfzmlbp  12319  fzofzim  12382  elfznelfzo  12439  injresinj  12451  subfzo0  12452  flval3  12478  modirr  12603  modsumfzodifsn  12605  addmodlteq  12607  ssnn0fi  12646  seqf1o  12704  expcl2lem  12734  expnegz  12756  expaddz  12766  expmulz  12768  facwordi  12938  faclbnd4lem4  12945  bccl  12971  hashnfinnn0  13013  hashgt12el  13070  hashgt12el2  13071  hashfun  13084  hashbclem  13093  hashbc  13094  hashfacen  13095  hashf1lem1  13096  hashf1  13098  hash2pwpr  13115  fundmge2nop0  13129  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  wrdind  13328  wrd2ind  13329  reuccats1  13332  swrdccatin1  13334  swrdccatin2  13338  swrdccat3  13343  swrdccat3blem  13346  cshw1  13419  cshwcsh2id  13425  wwlktovfo  13549  s3iunsndisj  13555  rtrclreclem3  13648  dfrtrcl2  13650  sqrlem1  13831  sqrlem6  13836  rexanre  13934  cau3lem  13942  2clim  14151  summo  14295  fsum2dlem  14343  fsumiun  14394  prodmo  14505  fprod2dlem  14549  bpolycl  14622  rpnnen2lem12  14793  odd2np1lem  14902  oddge22np1  14911  sqoddm1div8z  14916  sumeven  14948  pwp1fsum  14952  bitsfzo  14995  sadcaddlem  15017  gcd0id  15078  algcvgblem  15128  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  coprmproddvdslem  15214  divgcdcoprm0  15217  isprm7  15258  prmdvdsexpr  15267  prmfac1  15269  qnumdencl  15285  hashdvds  15318  prm23lt5  15357  pcneg  15416  prmpwdvds  15446  prmreclem2  15459  4sqlem12  15498  vdwlem6  15528  vdwlem10  15532  vdwlem13  15535  0ram  15562  ram0  15564  ramz  15567  ramcl  15571  prmgaplem3  15595  prmgaplem4  15596  prmgaplem5  15597  prmgaplem6  15598  cshwshashlem1  15640  prmlem0  15650  firest  15916  imasaddfnlem  16011  imasvscafn  16020  mremre  16087  cicsym  16287  initoid  16478  termoid  16479  iszeroi  16482  drsdirfi  16761  pospo  16796  joinfval  16824  meetfval  16838  lubun  16946  odupos  16958  acsfiindd  17000  psss  17037  mnd1id  17155  dfgrp2e  17271  dfgrp3lem  17336  symgfix2  17659  f1omvdco2  17691  symggen  17713  odcau  17842  pgpfi  17843  sylow2blem3  17860  sylow3lem2  17866  lsmmod  17911  efgsfo  17975  frgpuptinv  18007  frgpnabllem1  18099  cyggeninv  18108  lt6abl  18119  cyggex2  18121  gsumval3lem2  18130  gsumval3  18131  gsum2d2  18196  dmdprdd  18221  dprd2da  18264  pgpfac1lem5  18301  pgpfac  18306  srgbinomlem4  18366  dvdsrtr  18475  dvdsrmul1  18476  lss1d  18784  lspsolvlem  18963  lspsnat  18966  lbsextlem2  18980  lbsextlem3  18981  0ring  19091  01eq0ring  19093  0ring01eqbi  19094  rng1nfld  19099  domnmuln0  19119  abvn0b  19123  mvrf1  19246  mplcoe5lem  19288  opsrtoslem2  19306  cply1mul  19485  coe1fzgsumdlem  19492  gsummoncoe1  19495  pf1ind  19540  evl1gsumdlem  19541  xrsdsreclblem  19611  qsssubdrg  19624  prmirredlem  19660  cygznlem3  19737  obslbs  19893  dsmmacl  19904  lindfrn  19979  lmiclbs  19995  lmisfree  20000  matecl  20050  mat1dimelbas  20096  scmateALT  20137  mdetdiaglem  20223  mdet0  20231  mdetunilem9  20245  gsummatr01  20284  cpmatmcllem  20342  m2cpminvid2lem  20378  pmatcollpw3fi1lem2  20411  chfacfscmul0  20482  chfacfpmmul0  20486  cayhamlem3  20511  tgcl  20584  tgidm  20595  indistopon  20615  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  epttop  20623  opnnei  20734  neiptopnei  20746  tgrest  20773  restntr  20796  perfopn  20799  ordtrest2lem  20817  isreg2  20991  lmmo  20994  ordthauslem  20997  cmpsublem  21012  cmpsub  21013  cmpcld  21015  hauscmplem  21019  iunconlem  21040  uncon  21042  2ndcrest  21067  2ndcctbss  21068  2ndcdisj  21069  dis2ndc  21073  locfincmp  21139  comppfsc  21145  txbas  21180  ptbasin  21190  ptbasfi  21194  txcls  21217  txbasval  21219  ptpjopn  21225  ptclsg  21228  dfac14lem  21230  xkoccn  21232  txcnp  21233  txindis  21247  txdis1cn  21248  tx1stc  21263  tx2ndc  21264  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  txcon  21302  fbfinnfr  21455  opnfbas  21456  filtop  21469  isfild  21472  fbunfip  21483  filcon  21497  fbasrn  21498  filuni  21499  isufil2  21522  filssufilg  21525  ufileu  21533  filufint  21534  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  hausflimi  21594  hauspwpwf1  21601  flffbas  21609  flftg  21610  alexsublem  21658  alexsubALTlem1  21661  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem3  21668  cldsubg  21724  qustgpopn  21733  tgptsmscld  21764  tsmsxplem1  21766  ustfilxp  21826  imasdsf1olem  21988  bldisj  22013  xbln0  22029  prdsxmslem2  22144  xrsblre  22422  icccmplem2  22434  reconn  22439  opnreen  22442  xrge0tsms  22445  metdsre  22464  iccpnfcnv  22551  cnheiborlem  22561  phtpc01  22604  pi1blem  22647  tchcph  22844  cfilfcls  22880  iscau4  22885  bcthlem5  22933  bcth3  22936  hlhil  23022  ovolctb  23065  ovoliunlem2  23078  ovoliunnul  23082  ovolicc2  23097  volfiniun  23122  iundisj  23123  dyadmax  23172  dyadmbllem  23173  vitalilem2  23184  ismbfd  23213  mbfimaopnlem  23228  itg11  23264  i1faddlem  23266  mbfi1fseqlem4  23291  bddmulibl  23411  limciun  23464  perfdvf  23473  rolle  23557  dvivthlem1  23575  dvne0  23578  lhop1  23581  lhop2  23582  itgsubst  23616  dvdsq1p  23724  fta1g  23731  dgrco  23835  plydivex  23856  fta1  23867  ulmcaulem  23952  abelthlem2  23990  pilem2  24010  cxpmul2z  24237  cxpcn3lem  24288  xrlimcnp  24495  jensen  24515  wilthlem2  24595  wilthlem3  24596  muval2  24660  sqf11  24665  ppiublem1  24727  fsumvma  24738  lgsdir2lem2  24851  lgsdir2lem5  24854  lgsqrmodndvds  24878  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  gausslemma2d  24899  2lgsoddprmlem2  24934  dchrisum0fno1  25000  pntlem3  25098  pntleml  25100  ostthlem1  25116  ostth2lem2  25123  colinearalg  25590  axcontlem2  25645  axcontlem8  25651  edgupgr  25808  umgrpredgav  25813  usgrares1  25939  nbgraf1olem5  25974  cusgrarn  25988  nbcusgra  25992  uvtxnbgra  26021  wlkcpr  26057  3v3e3cycl2  26192  usg2wlkeq  26236  wlkiswwlksur  26247  clwlkswlks  26286  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  clwwlkf1  26324  erclwwlktr  26343  erclwwlkntr  26355  hashecclwwlkn1  26361  usghashecclwwlk  26362  wlklenvclwlk  26366  clwlkfoclwwlk  26372  vdusgra0nedg  26435  nbhashuvtx  26443  usgravd0nedg  26445  usgravd00  26446  rusgranumwlklem1  26476  3cyclfrgrarn1  26539  frgranbnb  26547  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  frgrancvvdeqlemC  26566  frgrawopreglem3  26573  frgrawopreglem5  26575  frgrawopreg2  26578  2spotiundisj  26589  2spotmdisj  26595  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  lnon0  27037  shmodsi  27632  shlub  27657  spanunsni  27822  h1datomi  27824  stm1ri  28487  stadd3i  28491  mdsl1i  28564  cvmdi  28567  superpos  28597  chjatom  28600  chirredi  28637  atcvat4i  28640  sumdmdii  28658  sumdmdlem  28661  cdj3lem2a  28679  cdj3lem3a  28682  cdj3i  28684  disji2f  28772  disjif2  28776  iundisjf  28784  rnmpt2ss  28856  iundisjfi  28942  nn0min  28954  xrge0tsmsd  29116  cnre2csqima  29285  ordtrest2NEWlem  29296  xrge0iifcnv  29307  lmxrge0  29326  measdivcstOLD  29614  dya2iocuni  29672  omssubadd  29689  eulerpartlems  29749  bnj849  30249  bnj1118  30306  derangenlem  30407  erdszelem9  30435  pconcon  30467  iccllyscon  30486  cvmsval  30502  cvmscld  30509  cvmsss2  30510  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift3lem5  30559  cvmlift3lem8  30562  msubvrs  30711  mthmblem  30731  untsucf  30841  3orel1  30846  3orel2  30847  3orel3  30848  nepss  30854  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  rdgprc  30944  trpredtr  30974  dftrpred3g  30977  trpredrec  30982  frmin  30983  frind  30984  frins2fg  30988  wzel  31015  wsuclem  31017  wsuclemOLD  31018  frrlem5e  31032  nosepon  31066  nodenselem4  31083  nodenselem8  31087  nocvxmin  31090  nofulllem5  31105  funpartfun  31220  altopth1  31242  altopth2  31243  colineardim1  31338  lineext  31353  btwnconn1lem14  31377  brsegle  31385  hilbert1.2  31432  trer  31480  elicc3  31481  finminlem  31482  fneint  31513  fnessref  31522  refssfne  31523  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  fnemeet2  31532  fnejoin2  31534  tailfb  31542  arg-ax  31585  ordtoplem  31604  onsuct0  31610  bj-gl4lem  31752  bj-sngltag  32164  bj-restn0  32224  bj-bary1lem1  32338  icorempt2  32375  icoreresf  32376  relowlssretop  32387  finxpreclem6  32409  fin2so  32566  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  mblfinlem1  32616  mblfinlem4  32619  ovoliunnfl  32621  itg2addnclem  32631  itg2addnclem2  32632  areacirc  32675  unirep  32677  filbcmb  32705  sdclem1  32709  fdc  32711  nninfnub  32717  isbnd2  32752  ssbnd  32757  prdsbnd2  32764  cntotbnd  32765  heibor1lem  32778  heiborlem1  32780  heiborlem4  32783  heiborlem6  32785  0idl  32994  intidl  32998  unichnidl  33000  keridl  33001  prnc  33036  prtlem17  33179  prter2  33184  ax12indn  33246  lsatn0  33304  lsatcmp  33308  lssat  33321  lfl1  33375  lshpsmreu  33414  lkrin  33469  glbconxN  33682  cvrat4  33747  paddasslem17  34140  pmodlem2  34151  dalawlem14  34188  pclclN  34195  pclfinN  34204  pclfinclN  34254  poml4N  34257  osumcllem8N  34267  pexmidlem5N  34278  cdleme32a  34747  cdlemg33b0  35007  tendoeq2  35080  diaelrnN  35352  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem2N  35601  dochvalr  35664  dochkrshp  35693  lcfl6  35807  lcfrvalsnN  35848  mapdordlem2  35944  mapdh8b  36087  mapdh9a  36097  hdmap14lem13  36190  eldioph2b  36344  eldiophss  36356  diophren  36395  ctbnfien  36400  rencldnfilem  36402  pellexlem3  36413  pellexlem5  36415  pellex  36417  pell14qrexpcl  36449  pellfundre  36463  pellfundge  36464  pellfundlb  36466  pellfundglb  36467  jm2.19lem4  36577  fnwe2lem2  36639  pwssplit4  36677  hbtlem5  36717  ss2iundf  36970  relexpmulg  37021  relexpxpmin  37028  relexpaddss  37029  dftrcl3  37031  dfrtrcl3  37044  clsk1indlem3  37361  isotone1  37366  isotone2  37367  ntrneiel2  37404  ntrneik4w  37418  onfrALT  37785  ax6e2ndeq  37796  snssiALT  38085  hirstL-ax3  39708  2reurex  39830  iccpartiltu  39960  iccpartigtl  39961  iccpartltu  39963  fmtnofac2lem  40018  fmtno4prmfac  40022  prmdvdsfmtnof1lem1  40034  lighneallem2  40061  opoeALTV  40132  opeoALTV  40133  gbegt5  40183  gbogt5  40184  bgoldbwt  40199  bgoldbst  40200  sgoldbalt  40203  nnsum3primesle9  40210  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem1  40221  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxccat3  40289  pfxccat3a  40292  reuccatpfxs1  40297  elnelall  40302  ralnralall  40307  otiunsndisjX  40317  fpropnf1  40337  subsubelfzo0  40359  ausgrumgri  40397  ausgrusgri  40398  ushgredgedga  40456  ushgredgedgaloop  40458  uhgr0v0e  40464  subumgredg2  40509  uhgrspan1  40527  fusgrfisstep  40548  nbuhgr  40565  nbuhgr2vtx1edgb  40574  uhgrnbgr0nb  40576  edgnbusgreu  40595  nbusgredgeu0  40596  nbusgrf1o0  40597  nbusgrvtxm1uvtx  40632  cusgredg  40646  cusgrfi  40674  usgredgsscusgredg  40675  1loopgrnb0  40717  usgrvd0nedg  40749  uhgrvd00  40750  upgr1wlkwlk  40847  upgr1wlkcompim  40851  uspgr2wlkeq  40854  uspgr2wlkeqi  40856  1wlkv0  40859  1wlklenvclwlk  40863  1wlkp1lem6  40887  lfgrwlkprop  40896  spthdep  40940  upgrwlkdvdelem  40942  usgr2wlkneq  40962  usgr2trlncl  40966  pthdlem1  40972  pthdlem2lem  40973  clwlkl1loop  40989  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0  41024  0enwwlksnge1  41060  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  wlkwwlksur  41094  umgr2adedgspth  41155  wwlks2onv  41158  2wspiundisj  41166  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  clwwlksf1  41224  erclwwlkstr  41243  erclwwlksntr  41255  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfoclwwlk  41270  eucrctshift  41411  3cyclfrgrrn1  41455  frgrnbnb  41463  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  frgrncvvdeqlemC  41478  frgrwopreglem3  41483  frgrwopreglem5  41485  frgrwopreg1  41487  frgrwopreg2  41488  2wspmdisj  41501  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  mgmpropd  41565  copisnmnd  41599  mgm2mgm  41653  ringrng  41669  c0snmgmhm  41704  ztprmneprm  41918  mndpsuppss  41946  lindslinindimp2lem4  42044  lindslinindsimp2  42046  lindsrng01  42051  snlindsntor  42054  ldepspr  42056  isldepslvec2  42068  suppdm  42094  blen1b  42180  dignn0ldlem  42194  digexp  42199  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  iunord  42220  tfis2d  42225
  Copyright terms: Public domain W3C validator