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

Theorem syl5bi 230
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 204 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 33 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3imtr4g  283  ancomsd  468  3jao  1380  nfimd  1810  axc16nf  2119  ax13  2231  2euex  2527  2eu1  2536  eqneqall  2788  necon3bd  2791  pm2.61dne  2863  spcimgft  3252  rspc  3271  rspcimdv  3278  euind  3355  reuind  3373  sbciegft  3428  rspsbc  3479  ssexnelpss  3677  pwpw0  4279  sssn  4291  eqsnOLD  4295  prel12  4314  prnebg  4320  pwsnALT  4357  intss1  4417  intmin  4422  uniintsn  4439  iinss  4497  iinss2  4498  disji2  4559  disjiun  4563  disjxiun  4569  disjxiunOLD  4570  trel3  4678  trin  4681  trintss  4687  eusvnfb  4779  reusv3  4793  copsexg  4872  otiunsndisj  4892  po3nr  4959  fri  4986  wefrc  5018  wereu2  5021  ssrelrel  5128  relop  5178  iss  5350  restidsingOLD  5361  poirr2  5422  xpcan  5471  xpcan2  5472  sossfld  5481  wfi  5612  wfis2fg  5616  onfr  5662  onmindif  5714  funopg  5818  funssres  5826  funun  5828  fv3  6097  fvmptt  6189  iinpreima  6234  fvn0ssdmfun  6239  dff3  6261  dff4  6262  fmptsng  6313  fmptsnd  6314  tpres  6345  fnprb  6351  fntpb  6352  fvclss  6378  isomin  6461  isofrlem  6464  weniso  6478  oprabid  6550  ssorduni  6850  onmindif2  6877  limuni3  6917  tfis2f  6920  tfinds  6924  tfinds2  6928  tfinds3  6929  funcnvuni  6985  f1oweALT  7016  f1o2ndf1  7145  poxp  7149  soxp  7150  fnse  7154  suppimacnv  7166  mpt2xopynvov0g  7200  reldmtpos  7220  rntpos  7225  wfrlem14  7288  wfrlem15  7289  onfununi  7298  smoiun  7318  tfrlem1  7332  tfr3  7355  frsucmptn  7394  tz7.49  7400  oaordi  7486  oawordeulem  7494  omeulem1  7522  oeordi  7527  oelimcl  7540  nnaordi  7558  nneob  7592  omsmolem  7593  erdisj  7654  qsss  7668  uniinqs  7687  map0g  7756  resixpfo  7805  ixpsnf1o  7807  xpdom3  7916  mapdom3  7990  phplem4  8000  php3  8004  unxpdomlem3  8024  ssfi  8038  findcard2  8058  findcard3  8061  frfi  8063  isfiniteg  8078  xpfi  8089  fiint  8095  finsschain  8129  dffi2  8185  marypha1lem  8195  marypha2  8201  supmo  8214  suplub2  8223  infmo  8257  ordiso2  8276  ordtypelem7  8285  ordtypelem8  8286  brwdom2  8334  unxpwdom2  8349  ixpiunwdom  8352  elirrv  8360  suc11reg  8372  noinfep  8413  cantnfle  8424  cantnflem1  8442  cantnf  8446  trcl  8460  epfrs  8463  rankpwi  8542  rankunb  8569  rankuni2b  8572  rankxplim3  8600  cplem1  8608  karden  8614  carddom2  8659  fseqenlem2  8704  ac10ct  8713  acni2  8725  acndom  8730  infpwfien  8741  alephordi  8753  alephord  8754  iunfictbso  8793  aceq3lem  8799  dfac5  8807  dfac2  8809  dfac12lem3  8823  dfac12r  8824  cdainflem  8869  cdainf  8870  cfub  8927  cfeq0  8934  coflim  8939  cfslb2n  8946  cofsmo  8947  coftr  8951  infpssr  8986  fin23lem7  8994  fin23lem11  8995  fin23lem21  9017  isf32lem2  9032  isf34lem4  9055  isfin1-2  9063  isfin1-3  9064  fin1a2lem9  9086  fin1a2lem11  9088  fin1a2lem12  9089  fin1a2lem13  9090  domtriomlem  9120  axdc3lem2  9129  axcclem  9135  ac6c4  9159  zorn2lem4  9177  zorn2lem5  9178  zorn2lem7  9180  ttukeylem5  9191  ttukeyg  9195  brdom6disj  9208  fnrndomg  9212  iunfo  9213  iundom2g  9214  ficard  9239  konigthlem  9242  alephval2  9246  pwcfsdom  9257  fpwwe2lem9  9312  fpwwe2lem11  9314  fpwwe2lem12  9315  fpwwe2lem13  9316  pwfseqlem3  9334  gchpwdom  9344  winalim2  9370  gchina  9373  wunex2  9412  tskr1om2  9442  tskxpss  9446  inar1  9449  tskuni  9457  gruun  9480  grudomon  9491  grur1  9494  ltmpi  9578  ltexprlem2  9711  ltexprlem6  9715  reclem2pr  9722  reclem3pr  9723  reclem4pr  9724  suplem1pr  9726  mulgt0sr  9778  supsrlem  9784  axrrecex  9836  axpre-sup  9842  ltlen  9985  addid0  10297  negn0  10306  negf1o  10307  mulge0b  10738  supaddc  10833  supadd  10834  supmul1  10835  supmullem1  10836  supmullem2  10837  supmul  10838  cju  10859  nnsub  10902  0mnnnnn0  11168  un0addcl  11169  un0mulcl  11170  nn0sub  11186  nn0n0n1ge2b  11202  peano5uzi  11294  eluzuzle  11524  zsupss  11605  qbtwnre  11859  xrsupexmnf  11959  xrinfmexpnf  11960  xrsupsslem  11961  xrinfmsslem  11962  xrub  11966  supxrun  11970  ixxdisj  12013  icodisj  12120  difreicc  12127  uzsubsubfz  12185  fzadd2  12198  elfzmlbp  12270  fzofzim  12333  elfznelfzo  12390  injresinj  12402  subfzo0  12403  flval3  12429  modirr  12554  modsumfzodifsn  12556  addmodlteq  12558  ssnn0fi  12597  seqf1o  12655  expcl2lem  12685  expnegz  12707  expaddz  12717  expmulz  12719  facwordi  12889  faclbnd4lem4  12896  bccl  12922  hashnfinnn0  12961  hashgt12el  13018  hashgt12el2  13019  hashfun  13032  hashbclem  13041  hashbc  13042  hashfacen  13043  hashf1lem1  13044  hashf1  13046  hash2pwpr  13061  fi1uzind  13076  brfi1indALT  13079  fi1uzindOLD  13082  brfi1indALTOLD  13085  wrdind  13270  wrd2ind  13271  reuccats1  13274  swrdccatin1  13276  swrdccatin2  13280  swrdccat3  13285  swrdccat3blem  13288  cshw1  13361  cshwcsh2id  13367  wwlktovfo  13491  s3iunsndisj  13497  rtrclreclem3  13590  dfrtrcl2  13592  sqrlem1  13773  sqrlem6  13778  rexanre  13876  cau3lem  13884  2clim  14093  summo  14237  fsum2dlem  14285  fsumiun  14336  prodmo  14447  fprod2dlem  14491  bpolycl  14564  rpnnen2lem12  14735  odd2np1lem  14844  oddge22np1  14853  sqoddm1div8z  14858  sumeven  14890  pwp1fsum  14894  bitsfzo  14937  sadcaddlem  14959  gcd0id  15020  algcvgblem  15070  lcmfunsnlem1  15130  lcmfunsnlem2lem1  15131  lcmfunsnlem2  15133  coprmproddvdslem  15156  divgcdcoprm0  15159  isprm7  15200  prmdvdsexpr  15209  prmfac1  15211  qnumdencl  15227  hashdvds  15260  prm23lt5  15299  pcneg  15358  prmpwdvds  15388  prmreclem2  15401  4sqlem12  15440  vdwlem6  15470  vdwlem10  15474  vdwlem13  15477  0ram  15504  ram0  15506  ramz  15509  ramcl  15513  prmgaplem3  15537  prmgaplem4  15538  prmgaplem5  15539  prmgaplem6  15540  cshwshashlem1  15582  prmlem0  15592  firest  15858  imasaddfnlem  15953  imasvscafn  15962  mremre  16029  cicsym  16229  initoid  16420  termoid  16421  iszeroi  16424  drsdirfi  16703  pospo  16738  joinfval  16766  meetfval  16780  lubun  16888  odupos  16900  acsfiindd  16942  psss  16979  mnd1id  17097  dfgrp2e  17213  dfgrp3lem  17278  symgfix2  17601  f1omvdco2  17633  symggen  17655  odcau  17784  pgpfi  17785  sylow2blem3  17802  sylow3lem2  17808  lsmmod  17853  efgsfo  17917  frgpuptinv  17949  frgpnabllem1  18041  cyggeninv  18050  lt6abl  18061  cyggex2  18063  gsumval3lem2  18072  gsumval3  18073  gsum2d2  18138  dmdprdd  18163  dprd2da  18206  pgpfac1lem5  18243  pgpfac  18248  srgbinomlem4  18308  dvdsrtr  18417  dvdsrmul1  18418  lss1d  18726  lspsolvlem  18905  lspsnat  18908  lbsextlem2  18922  lbsextlem3  18923  0ring  19033  01eq0ring  19035  0ring01eqbi  19036  rng1nfld  19041  domnmuln0  19061  abvn0b  19065  mvrf1  19188  mplcoe5lem  19230  opsrtoslem2  19248  cply1mul  19427  coe1fzgsumdlem  19434  gsummoncoe1  19437  pf1ind  19482  evl1gsumdlem  19483  xrsdsreclblem  19553  qsssubdrg  19566  prmirredlem  19601  cygznlem3  19678  obslbs  19831  dsmmacl  19842  lindfrn  19917  lmiclbs  19933  lmisfree  19938  matecl  19988  mat1dimelbas  20034  scmateALT  20075  mdetdiaglem  20161  mdet0  20169  mdetunilem9  20183  gsummatr01  20222  cpmatmcllem  20280  m2cpminvid2lem  20316  pmatcollpw3fi1lem2  20349  chfacfscmul0  20420  chfacfpmmul0  20424  cayhamlem3  20449  tgcl  20522  tgidm  20533  indistopon  20553  fctop  20556  cctop  20558  ppttop  20559  pptbas  20560  epttop  20561  opnnei  20672  neiptopnei  20684  tgrest  20711  restntr  20734  perfopn  20737  ordtrest2lem  20755  isreg2  20929  lmmo  20932  ordthauslem  20935  cmpsublem  20950  cmpsub  20951  cmpcld  20953  hauscmplem  20957  iunconlem  20978  uncon  20980  2ndcrest  21005  2ndcctbss  21006  2ndcdisj  21007  dis2ndc  21011  locfincmp  21077  comppfsc  21083  txbas  21118  ptbasin  21128  ptbasfi  21132  txcls  21155  txbasval  21157  ptpjopn  21163  ptclsg  21166  dfac14lem  21168  xkoccn  21170  txcnp  21171  txindis  21185  txdis1cn  21186  tx1stc  21201  tx2ndc  21202  txkgen  21203  xkoco1cn  21208  xkoco2cn  21209  xkococn  21211  xkoinjcn  21238  txcon  21240  fbfinnfr  21393  opnfbas  21394  filtop  21407  isfild  21410  fbunfip  21421  filcon  21435  fbasrn  21436  filuni  21437  isufil2  21460  filssufilg  21463  ufileu  21471  filufint  21472  rnelfmlem  21504  rnelfm  21505  fmfnfmlem2  21507  fmfnfmlem4  21509  fmfnfm  21510  hausflimi  21532  hauspwpwf1  21539  flffbas  21547  flftg  21548  alexsublem  21596  alexsubALTlem1  21599  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALTlem4  21602  alexsubALT  21603  ptcmplem3  21606  cldsubg  21662  qustgpopn  21671  tgptsmscld  21702  tsmsxplem1  21704  ustfilxp  21764  imasdsf1olem  21925  bldisj  21950  xbln0  21966  prdsxmslem2  22081  xrsblre  22350  icccmplem2  22362  reconn  22367  opnreen  22370  xrge0tsms  22373  metdsre  22391  iccpnfcnv  22478  cnheiborlem  22488  phtpc01  22531  pi1blem  22574  tchcph  22761  cfilfcls  22794  iscau4  22799  bcthlem5  22846  bcth3  22849  hlhil  22935  ovolctb  22978  ovoliunlem2  22991  ovoliunnul  22995  ovolicc2  23010  volfiniun  23035  iundisj  23036  dyadmax  23085  dyadmbllem  23086  vitalilem2  23097  ismbfd  23126  mbfimaopnlem  23141  itg11  23177  i1faddlem  23179  mbfi1fseqlem4  23204  bddmulibl  23324  limciun  23377  perfdvf  23386  rolle  23470  dvivthlem1  23488  dvne0  23491  lhop1  23494  lhop2  23495  itgsubst  23529  dvdsq1p  23637  fta1g  23644  dgrco  23748  plydivex  23769  fta1  23780  ulmcaulem  23865  abelthlem2  23903  pilem2  23923  cxpmul2z  24150  cxpcn3lem  24201  xrlimcnp  24408  jensen  24428  wilthlem2  24508  wilthlem3  24509  muval2  24573  sqf11  24578  ppiublem1  24640  fsumvma  24651  lgsdir2lem2  24764  lgsdir2lem5  24767  lgsqrmodndvds  24791  gausslemma2dlem1a  24803  gausslemma2dlem3  24806  gausslemma2d  24812  2lgsoddprmlem2  24847  dchrisum0fno1  24913  pntlem3  25011  pntleml  25013  ostthlem1  25029  ostth2lem2  25036  colinearalg  25504  axcontlem2  25559  axcontlem8  25565  usgrares1  25701  nbgraf1olem5  25736  cusgrarn  25750  nbcusgra  25754  uvtxnbgra  25783  wlkcpr  25819  3v3e3cycl2  25954  usg2wlkeq  25998  wlkiswwlksur  26009  clwlkswlks  26048  clwlkisclwwlklem2a4  26074  clwlkisclwwlklem1  26077  clwwlkf1  26086  erclwwlktr  26105  erclwwlkntr  26117  hashecclwwlkn1  26123  usghashecclwwlk  26124  wlklenvclwlk  26128  clwlkfoclwwlk  26134  vdusgra0nedg  26197  nbhashuvtx  26205  usgravd0nedg  26207  usgravd00  26208  rusgranumwlklem1  26238  3cyclfrgrarn1  26301  frgranbnb  26309  frgrancvvdeqlem3  26321  frgrancvvdeqlem4  26322  frgrancvvdeqlemC  26328  frgrawopreglem3  26335  frgrawopreglem5  26337  frgrawopreg2  26340  2spotiundisj  26351  2spotmdisj  26357  extwwlkfablem2  26367  numclwwlkovf2ex  26375  numclwlk1lem2f1  26383  lnon0  26839  shmodsi  27434  shlub  27459  spanunsni  27624  h1datomi  27626  stm1ri  28289  stadd3i  28293  mdsl1i  28366  cvmdi  28369  superpos  28399  chjatom  28402  chirredi  28439  atcvat4i  28442  sumdmdii  28460  sumdmdlem  28463  cdj3lem2a  28481  cdj3lem3a  28484  cdj3i  28486  disji2f  28574  disjif2  28578  iundisjf  28586  rnmpt2ss  28658  iundisjfi  28744  nn0min  28756  xrge0tsmsd  28918  cnre2csqima  29087  ordtrest2NEWlem  29098  xrge0iifcnv  29109  lmxrge0  29128  measdivcstOLD  29416  dya2iocuni  29474  omssubadd  29491  eulerpartlems  29551  bnj849  30051  bnj1118  30108  derangenlem  30209  erdszelem9  30237  pconcon  30269  iccllyscon  30288  cvmsval  30304  cvmscld  30311  cvmsss2  30312  cvmopnlem  30316  cvmfolem  30317  cvmliftmolem2  30320  cvmlift2lem10  30350  cvmlift2lem12  30352  cvmlift3lem5  30361  cvmlift3lem8  30364  msubvrs  30513  mthmblem  30533  untsucf  30643  3orel1  30648  3orel2  30649  3orel3  30650  nepss  30656  dfon2lem5  30738  dfon2lem6  30739  dfon2lem7  30740  dfon2lem8  30741  rdgprc  30746  trpredtr  30776  dftrpred3g  30779  trpredrec  30784  frmin  30785  frind  30786  frins2fg  30790  wzel  30817  wsuclem  30819  wsuclemOLD  30820  frrlem5e  30834  nosepon  30868  nodenselem4  30885  nodenselem8  30889  nocvxmin  30892  nofulllem5  30907  funpartfun  31022  altopth1  31044  altopth2  31045  colineardim1  31140  lineext  31155  btwnconn1lem14  31179  brsegle  31187  hilbert1.2  31234  trer  31282  elicc3  31283  finminlem  31284  fneint  31315  fnessref  31324  refssfne  31325  neibastop1  31326  neibastop2lem  31327  neibastop2  31328  fnemeet2  31334  fnejoin2  31336  tailfb  31344  arg-ax  31387  ordtoplem  31406  onsuct0  31412  bj-gl4lem  31554  bj-sngltag  31963  bj-restn0  32023  bj-bary1lem1  32137  icorempt2  32174  icoreresf  32175  relowlssretop  32186  finxpreclem6  32208  fin2so  32365  poimirlem24  32402  poimirlem25  32403  poimirlem26  32404  poimirlem27  32405  poimirlem29  32407  poimirlem30  32408  poimirlem31  32409  mblfinlem1  32415  mblfinlem4  32418  ovoliunnfl  32420  itg2addnclem  32430  itg2addnclem2  32431  areacirc  32474  unirep  32476  filbcmb  32504  sdclem1  32508  fdc  32510  nninfnub  32516  isbnd2  32551  ssbnd  32556  prdsbnd2  32563  cntotbnd  32564  heibor1lem  32577  heiborlem1  32579  heiborlem4  32582  heiborlem6  32584  0idl  32793  intidl  32797  unichnidl  32799  keridl  32800  prnc  32835  prtlem17  32978  prter2  32983  ax12indn  33045  lsatn0  33103  lsatcmp  33107  lssat  33120  lfl1  33174  lshpsmreu  33213  lkrin  33268  glbconxN  33481  cvrat4  33546  paddasslem17  33939  pmodlem2  33950  dalawlem14  33987  pclclN  33994  pclfinN  34003  pclfinclN  34053  poml4N  34056  osumcllem8N  34066  pexmidlem5N  34077  cdleme32a  34546  cdlemg33b0  34806  tendoeq2  34879  diaelrnN  35151  dihmeetlem1N  35396  dihglblem5apreN  35397  dihglblem2N  35400  dochvalr  35463  dochkrshp  35492  lcfl6  35606  lcfrvalsnN  35647  mapdordlem2  35743  mapdh8b  35886  mapdh9a  35896  hdmap14lem13  35989  eldioph2b  36143  eldiophss  36155  diophren  36194  ctbnfien  36199  rencldnfilem  36201  pellexlem3  36212  pellexlem5  36214  pellex  36216  pell14qrexpcl  36248  pellfundre  36262  pellfundge  36263  pellfundlb  36265  pellfundglb  36266  jm2.19lem4  36376  fnwe2lem2  36438  pwssplit4  36476  hbtlem5  36516  ss2iundf  36769  relexpmulg  36820  relexpxpmin  36827  relexpaddss  36828  dftrcl3  36830  dfrtrcl3  36843  clsk1indlem3  37160  isotone1  37165  isotone2  37166  ntrneiel2  37203  ntrneik4w  37217  onfrALT  37584  ax6e2ndeq  37595  snssiALT  37884  hirstL-ax3  39508  2reurex  39630  iccpartiltu  39761  iccpartigtl  39762  iccpartltu  39764  fmtnofac2lem  39819  fmtno4prmfac  39823  prmdvdsfmtnof1lem1  39835  lighneallem2  39862  opoeALTV  39933  opeoALTV  39934  gbegt5  39984  gbogt5  39985  bgoldbwt  40000  bgoldbst  40001  sgoldbalt  40004  nnsum3primesle9  40011  nnsum4primeseven  40017  nnsum4primesevenALTV  40018  wtgoldbnnsum4prm  40019  bgoldbnnsum3prm  40021  bgoldbtbndlem1  40022  bgoldbtbndlem4  40025  bgoldbtbnd  40026  pfxccat3  40090  pfxccat3a  40093  reuccatpfxs1  40098  elnelall  40103  ralnralall  40108  propeqop  40122  iunopeqop  40127  otiunsndisjX  40128  fundmge2nop0  40148  fpropnf1  40160  subsubelfzo0  40182  edgupgr  40365  umgrpredgav  40370  ausgrumgri  40395  ausgrusgri  40396  ushgredgedga  40454  ushgredgedgaloop  40456  uhgr0v0e  40462  subumgredg2  40507  uhgrspan1  40525  fusgrfisstep  40546  nbuhgr  40563  nbuhgr2vtx1edgb  40572  uhgrnbgr0nb  40574  edgnbusgreu  40593  nbusgredgeu0  40594  nbusgrf1o0  40595  nbusgrvtxm1uvtx  40630  cusgredg  40644  cusgrfi  40672  usgredgsscusgredg  40673  1loopgrnb0  40715  usgrvd0nedg  40747  uhgrvd00  40748  upgr1wlkwlk  40845  upgr1wlkcompim  40849  uspgr2wlkeq  40852  uspgr2wlkeqi  40854  1wlkv0  40857  1wlklenvclwlk  40861  1wlkp1lem6  40885  lfgrwlkprop  40894  spthdep  40938  upgrwlkdvdelem  40940  usgr2wlkneq  40960  usgr2trlncl  40964  pthdlem1  40970  pthdlem2lem  40971  clwlkl1loop  40987  crctcsh1wlkn0lem3  41013  crctcsh1wlkn0lem5  41015  crctcsh1wlkn0  41022  0enwwlksnge1  41058  1wlkiswwlks2  41070  1wlkiswwlksupgr2  41072  wlkwwlksur  41092  umgr2adedgspth  41153  wwlks2onv  41156  2wspiundisj  41164  clwlkclwwlklem2a4  41204  clwlkclwwlklem2  41207  clwwlksf1  41222  erclwwlkstr  41241  erclwwlksntr  41253  hashecclwwlksn1  41259  umgrhashecclwwlk  41260  clwlksfoclwwlk  41268  eucrctshift  41409  3cyclfrgrrn1  41453  frgrnbnb  41461  frgrncvvdeqlem3  41469  frgrncvvdeqlem4  41470  frgrncvvdeqlemC  41476  frgrwopreglem3  41481  frgrwopreglem5  41483  frgrwopreg1  41485  frgrwopreg2  41486  2wspmdisj  41499  av-numclwwlkovf2ex  41515  av-numclwlk1lem2f1  41522  mgmpropd  41563  copisnmnd  41597  mgm2mgm  41651  ringrng  41667  c0snmgmhm  41702  ztprmneprm  41916  mndpsuppss  41944  lindslinindimp2lem4  42042  lindslinindsimp2  42044  lindsrng01  42049  snlindsntor  42052  ldepspr  42054  isldepslvec2  42066  suppdm  42092  blen1b  42178  dignn0ldlem  42192  digexp  42197  nn0sumshdiglemB  42210  nn0sumshdiglem1  42211
  Copyright terms: Public domain W3C validator