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

Theorem syl5bi 233
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 207 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr4g  287  ancomsd  453  3orel1  1104  3jaoOLD  1543  nfimdOLDOLD  1985  axc16nf  2316  ax13  2425  2euex  2715  2eu1  2724  eqneqall  2996  necon3bd  2999  pm2.61dne  3071  elnelall  3101  spcimgft  3484  rspc  3503  rspcimdv  3510  rspc2gv  3521  euind  3598  reuind  3616  sbciegft  3671  rspsbc  3720  ssexnelpss  3925  ralnralall  4280  pwpw0  4541  sssn  4554  prel12OLD  4577  prnebg  4583  pwsnALT  4630  intss1  4691  intmin  4696  uniintsn  4713  iinss  4770  iinss2  4771  disji2  4835  disjiun  4839  disjiund  4842  disjxiun  4848  trel3  4961  trin  4963  trintssOLD  4970  eusvnfb  5069  reusv3  5081  copsexg  5152  propeqop  5169  otiunsndisj  5182  iunopeqop  5183  po3nr  5253  fri  5280  wefrc  5312  wereu2  5315  ssrelrel  5429  relop  5481  iss  5659  poirr2  5738  xpcan  5788  xpcan2  5789  sossfld  5798  wfi  5933  wfis2fg  5937  onfr  5982  onmindif  6033  funopg  6138  funssres  6147  funun  6149  fv3  6429  fvmptt  6524  iinpreima  6570  fvn0ssdmfun  6575  dff3  6597  dff4  6598  fmptsng  6662  fmptsnd  6663  tpres  6694  fnprb  6700  fntpb  6701  fvclss  6727  fpropnf1  6751  isomin  6814  isofrlem  6817  weniso  6831  oprabid  6908  ssorduni  7218  onmindif2  7245  limuni3  7285  tfis2f  7288  tfinds  7292  tfinds2  7296  tfinds3  7297  funcnvuni  7352  f1oweALT  7385  f1o2ndf1  7522  poxp  7526  soxp  7527  fnse  7531  suppimacnv  7543  mpt2xopynvov0g  7578  reldmtpos  7598  rntpos  7603  wfrlem14  7667  wfrlem15  7668  onfununi  7677  smoiun  7697  tfrlem1  7711  tfr3  7734  frsucmptn  7773  tz7.49  7779  oaordi  7866  oawordeulem  7874  omeulem1  7902  oeordi  7907  oelimcl  7920  nnaordi  7938  nneob  7972  omsmolem  7973  erdisj  8032  qsss  8046  uniinqs  8065  map0g  8136  resixpfo  8186  ixpsnf1o  8188  xpdom3  8300  mapdom3  8374  phplem4  8384  php3  8388  unxpdomlem3  8408  ssfi  8422  findcard2  8442  findcard3  8445  frfi  8447  isfiniteg  8462  xpfi  8473  fiint  8479  finsschain  8515  dffi2  8571  marypha1lem  8581  marypha2  8587  supmo  8600  suplub2  8609  infmo  8643  ordiso2  8662  ordtypelem7  8671  ordtypelem8  8672  brwdom2  8720  unxpwdom2  8735  ixpiunwdom  8738  elirrv  8743  suc11reg  8766  noinfep  8807  cantnfle  8818  cantnflem1  8836  cantnf  8840  trcl  8854  epfrs  8857  rankpwi  8936  rankunb  8963  rankuni2b  8966  rankxplim3  8994  cplem1  9002  karden  9008  carddom2  9089  fseqenlem2  9134  ac10ct  9143  acni2  9155  acndom  9160  infpwfien  9171  alephordi  9183  alephord  9184  iunfictbso  9223  aceq3lem  9229  dfac5  9237  dfac2b  9239  dfac2OLD  9241  dfac12lem3  9255  dfac12r  9256  cdainflem  9301  cdainf  9302  cfub  9359  cfeq0  9366  coflim  9371  cfslb2n  9378  cofsmo  9379  coftr  9383  infpssr  9418  fin23lem7  9426  fin23lem11  9427  fin23lem21  9449  isf32lem2  9464  isf34lem4  9487  isfin1-2  9495  isfin1-3  9496  fin1a2lem9  9518  fin1a2lem11  9520  fin1a2lem12  9521  fin1a2lem13  9522  domtriomlem  9552  axdc3lem2  9561  axcclem  9567  ac6c4  9591  zorn2lem4  9609  zorn2lem5  9610  zorn2lem7  9612  ttukeylem5  9623  ttukeyg  9627  brdom6disj  9642  fnrndomg  9646  iunfo  9649  iundom2g  9650  ficard  9675  konigthlem  9678  alephval2  9682  pwcfsdom  9693  fpwwe2lem9  9748  fpwwe2lem11  9750  fpwwe2lem12  9751  fpwwe2lem13  9752  pwfseqlem3  9770  gchpwdom  9780  winalim2  9806  gchina  9809  wunex2  9848  tskr1om2  9878  tskxpss  9882  inar1  9885  tskuni  9893  gruun  9916  grudomon  9927  grur1  9930  ltmpi  10014  ltexprlem2  10147  ltexprlem6  10151  reclem2pr  10158  reclem3pr  10159  reclem4pr  10160  suplem1pr  10162  mulgt0sr  10214  supsrlem  10220  axrrecex  10272  axpre-sup  10278  ltlen  10426  addid0  10738  negn0  10747  negf1o  10748  mulge0b  11181  supaddc  11278  supadd  11279  supmul1  11280  supmullem1  11281  supmullem2  11282  supmul  11283  cju  11304  nnsub  11348  0mnnnnn0  11594  un0addcl  11595  un0mulcl  11596  nn0sub  11612  nn0n0n1ge2b  11628  peano5uzi  11735  eluzuzle  11916  zsupss  11999  qbtwnre  12251  xrsupexmnf  12356  xrinfmexpnf  12357  xrsupsslem  12358  xrinfmsslem  12359  xrub  12363  supxrun  12367  ixxdisj  12411  icodisj  12521  difreicc  12530  uzsubsubfz  12589  fzadd2  12602  elfzmlbp  12677  fzofzim  12742  elfznelfzo  12800  injresinj  12816  subfzo0  12817  flval3  12843  modirr  12968  modsumfzodifsn  12970  addmodlteq  12972  ssnn0fi  13011  seqf1o  13068  expcl2lem  13098  expnegz  13120  expaddz  13130  expmulz  13132  facwordi  13299  faclbnd4lem4  13306  bccl  13332  hashnfinnn0  13373  hashgt12el  13430  hashgt12el2  13431  hashfun  13444  hashbclem  13456  hashbc  13457  hashfacen  13458  hashf1lem1  13459  hashf1  13461  hash2pwpr  13478  fundmge2nop0  13494  fi1uzind  13499  brfi1indALT  13502  wrdind  13703  wrd2ind  13704  reuccats1  13707  swrdccatin1  13710  swrdccatin2  13714  swrdccat3  13719  swrdccat3blem  13722  cshw1  13795  cshwcsh2id  13801  wwlktovfo  13929  s3iunsndisj  13935  rtrclreclem3  14026  dfrtrcl2  14028  sqrlem1  14209  sqrlem6  14214  rexanre  14312  cau3lem  14320  2clim  14529  summo  14674  fsum2dlem  14727  fsumiun  14778  prodmo  14890  fprod2dlem  14934  bpolycl  15006  rpnnen2lem12  15177  odd2np1lem  15287  oddge22np1  15296  sqoddm1div8z  15301  sumeven  15333  pwp1fsum  15337  bitsfzo  15379  sadcaddlem  15401  gcd0id  15462  algcvgblem  15512  lcmfunsnlem1  15572  lcmfunsnlem2lem1  15573  lcmfunsnlem2  15575  coprmproddvdslem  15597  divgcdcoprm0  15600  isprm7  15640  prmdvdsexpr  15649  prmfac1  15651  qnumdencl  15667  hashdvds  15700  prm23lt5  15739  pcneg  15798  prmpwdvds  15828  prmreclem2  15841  4sqlem12  15880  vdwlem6  15910  vdwlem10  15914  vdwlem13  15917  0ram  15944  ram0  15946  ramz  15949  ramcl  15953  prmgaplem3  15977  prmgaplem4  15978  prmgaplem5  15979  prmgaplem6  15980  cshwshashlem1  16017  prmlem0  16027  firest  16301  imasaddfnlem  16396  imasvscafn  16405  mremre  16472  cicsym  16671  initoid  16862  termoid  16863  iszeroi  16866  drsdirfi  17146  pospo  17181  joinfval  17209  meetfval  17223  lubun  17331  odupos  17343  acsfiindd  17385  psss  17422  mnd1id  17540  dfgrp2e  17656  dfgrp3lem  17721  symgfix2  18040  f1omvdco2  18072  symggen  18094  odcau  18223  pgpfi  18224  sylow2blem3  18241  sylow3lem2  18247  lsmmod  18292  efgsfo  18356  frgpuptinv  18388  frgpnabllem1  18480  cyggeninv  18489  lt6abl  18500  cyggex2  18502  gsumval3lem2  18511  gsumval3  18512  gsum2d2  18577  dmdprdd  18603  dprd2da  18646  pgpfac1lem5  18683  pgpfac  18688  srgbinomlem4  18748  dvdsrtr  18857  dvdsrmul1  18858  lss1d  19173  lspsolvlem  19353  lspsnat  19356  lbsextlem2  19371  lbsextlem3  19372  0ring  19482  01eq0ring  19484  0ring01eqbi  19485  rng1nfld  19490  domnmuln0  19510  abvn0b  19514  mvrf1  19637  mplcoe5lem  19679  opsrtoslem2  19696  cply1mul  19875  coe1fzgsumdlem  19882  gsummoncoe1  19885  pf1ind  19930  evl1gsumdlem  19931  xrsdsreclblem  20003  qsssubdrg  20016  prmirredlem  20052  cygznlem3  20128  obslbs  20288  dsmmacl  20299  lindfrn  20374  lmiclbs  20390  lmisfree  20395  matecl  20445  mat1dimelbas  20492  scmateALT  20533  mdetdiaglem  20619  mdet0  20627  mdetunilem9  20641  gsummatr01  20681  cpmatmcllem  20740  m2cpminvid2lem  20776  pmatcollpw3fi1lem2  20809  chfacfscmul0  20880  chfacfpmmul0  20884  cayhamlem3  20909  tgcl  20991  tgidm  21002  indistopon  21023  fctop  21026  cctop  21028  ppttop  21029  pptbas  21030  epttop  21031  opnnei  21142  neiptopnei  21154  tgrest  21181  restntr  21204  perfopn  21207  ordtrest2lem  21225  isreg2  21399  lmmo  21402  ordthauslem  21405  cmpsublem  21420  cmpsub  21421  cmpcld  21423  hauscmplem  21427  iunconnlem  21448  unconn  21450  2ndcrest  21475  2ndcctbss  21476  2ndcdisj  21477  dis2ndc  21481  locfincmp  21547  comppfsc  21553  txbas  21588  ptbasin  21598  ptbasfi  21602  txcls  21625  txbasval  21627  ptpjopn  21633  ptclsg  21636  dfac14lem  21638  xkoccn  21640  txcnp  21641  txindis  21655  txdis1cn  21656  tx1stc  21671  tx2ndc  21672  txkgen  21673  xkoco1cn  21678  xkoco2cn  21679  xkococn  21681  xkoinjcn  21708  txconn  21710  fbfinnfr  21862  opnfbas  21863  filtop  21876  isfild  21879  fbunfip  21890  filconn  21904  fbasrn  21905  filuni  21906  isufil2  21929  filssufilg  21932  ufileu  21940  filufint  21941  rnelfmlem  21973  rnelfm  21974  fmfnfmlem2  21976  fmfnfmlem4  21978  fmfnfm  21979  hausflimi  22001  hauspwpwf1  22008  flffbas  22016  flftg  22017  alexsublem  22065  alexsubALTlem1  22068  alexsubALTlem2  22069  alexsubALTlem3  22070  alexsubALTlem4  22071  alexsubALT  22072  ptcmplem3  22075  cldsubg  22131  qustgpopn  22140  tgptsmscld  22171  tsmsxplem1  22173  ustfilxp  22233  imasdsf1olem  22395  bldisj  22420  xbln0  22436  prdsxmslem2  22551  xrsblre  22831  icccmplem2  22843  reconn  22848  opnreen  22851  xrge0tsms  22854  metdsre  22873  iccpnfcnv  22960  cnheiborlem  22970  phtpc01  23012  pi1blem  23055  tchcph  23252  cfilfcls  23289  iscau4  23294  bcthlem5  23342  bcth3  23345  hlhil  23432  ovolctb  23477  ovoliunlem2  23490  ovoliunnul  23494  ovolicc2  23509  volfiniun  23534  iundisj  23535  dyadmax  23585  dyadmbllem  23586  vitalilem2  23596  ismbfd  23626  mbfimaopnlem  23642  itg11  23678  i1faddlem  23680  mbfi1fseqlem4  23705  bddmulibl  23825  limciun  23878  perfdvf  23887  rolle  23973  dvivthlem1  23991  dvne0  23994  lhop1  23997  lhop2  23998  itgsubst  24032  dvdsq1p  24140  fta1g  24147  dgrco  24251  plydivex  24272  fta1  24283  ulmcaulem  24368  abelthlem2  24406  pilem2  24426  cxpmul2z  24657  cxpcn3lem  24708  xrlimcnp  24915  jensen  24935  wilthlem2  25015  wilthlem3  25016  muval2  25080  sqf11  25085  ppiublem1  25147  fsumvma  25158  lgsdir2lem2  25271  lgsdir2lem5  25274  lgsqrmodndvds  25298  gausslemma2dlem1a  25310  gausslemma2dlem3  25313  gausslemma2d  25319  2lgsoddprmlem2  25354  dchrisum0fno1  25420  pntlem3  25518  pntleml  25520  ostthlem1  25536  ostth2lem2  25543  colinearalg  26010  axcontlem2  26065  axcontlem8  26071  edgupgr  26249  umgrpredgv  26256  numedglnl  26260  ausgrumgri  26283  ausgrusgri  26284  ushgredgedg  26342  ushgredgedgloop  26344  ushgredgedgloopOLD  26345  uhgr0v0e  26352  subumgredg2  26399  uhgrspansubgrlem  26404  uhgrspan1  26417  upgrreslem  26418  umgrreslem  26419  upgrres1  26427  fusgrfisstep  26443  nbuhgr  26461  nbuhgr2vtx1edgblem  26469  nbuhgr2vtx1edgb  26470  uhgrnbgr0nb  26472  edgnbusgreu  26490  edgnbusgreuOLD  26491  nbusgredgeu0  26492  nbusgrf1o0  26493  nbusgrvtxm1uvtx  26534  cusgredg  26554  cusgrfi  26588  usgredgsscusgredg  26589  1loopgrnb0  26632  usgrvd0nedg  26663  uhgrvd00  26664  upgriswlk  26771  upgrwlkcompim  26773  uspgr2wlkeq  26776  uspgr2wlkeqi  26778  wlkv0  26781  wlklenvclwlk  26785  wlkp1lem6  26809  lfgrwlkprop  26818  spthdep  26864  upgrwlkdvdelem  26866  usgr2wlkneq  26886  usgr2trlncl  26890  pthdlem1  26896  pthdlem2lem  26897  clwlkl1loop  26913  crctcshwlkn0lem3  26939  crctcshwlkn0lem5  26941  crctcshwlkn0  26948  0enwwlksnge1  26997  wlkiswwlks2  27008  wlkiswwlksupgr2  27010  wlkwwlksurOLD  27031  wspthsnonn0vne  27063  umgr2adedgspth  27094  clwlkclwwlklem2a4  27146  clwlkclwwlklem2  27149  clwlkclwwlkf  27157  clwlkclwwlkfo  27158  erclwwlktr  27171  clwwlkf1  27204  erclwwlkntr  27228  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  clwlksfoclwwlkOLD  27243  clwwlknonex2e  27285  eucrctshift  27422  3cyclfrgrrn1  27466  frgrnbnb  27474  frgrncvvdeqlem2  27481  frgrncvvdeqlem3  27482  frgrncvvdeqlem9  27488  frgrwopreglem4a  27491  frgrwopregbsn  27498  frgrwopreg1  27499  frgrwopreg2  27500  frgrwopreglem5lem  27501  frgrwopreglem5ALT  27503  frgr2wwlk1  27510  numclwwlk1lem2foa  27539  numclwwlk1lem2f1  27542  wlkl0  27553  lnon0  27987  shmodsi  28582  shlub  28607  spanunsni  28772  h1datomi  28774  stm1ri  29437  stadd3i  29441  mdsl1i  29514  cvmdi  29517  superpos  29547  chjatom  29550  chirredi  29587  atcvat4i  29590  sumdmdii  29608  sumdmdlem  29611  cdj3lem2a  29629  cdj3lem3a  29632  cdj3i  29634  disji2f  29721  disjif2  29725  iundisjf  29733  rnmpt2ss  29806  iundisjfi  29888  nn0min  29900  xrge0tsmsd  30116  cnre2csqima  30288  ordtrest2NEWlem  30299  xrge0iifcnv  30310  lmxrge0  30329  measdivcstOLD  30618  dya2iocuni  30676  omssubadd  30693  eulerpartlems  30753  bnj849  31323  bnj1118  31380  derangenlem  31481  erdszelem9  31509  pconnconn  31541  iccllysconn  31560  cvmsval  31576  cvmscld  31583  cvmsss2  31584  cvmopnlem  31588  cvmfolem  31589  cvmliftmolem2  31592  cvmlift2lem10  31622  cvmlift2lem12  31624  cvmlift3lem5  31633  cvmlift3lem8  31636  msubvrs  31785  mthmblem  31805  untsucf  31914  3orel2  31919  3orel3  31920  nepss  31926  eqfunresadj  31986  dfon2lem5  32017  dfon2lem6  32018  dfon2lem7  32019  dfon2lem8  32020  rdgprc  32025  trpredtr  32055  dftrpred3g  32058  trpredrec  32063  frpomin  32064  frpoind  32066  frmin  32068  frind  32069  frins2fg  32073  wzel  32095  wsuclem  32096  frrlem5e  32114  nosepon  32144  noextendseq  32146  nolesgn2ores  32151  nosepdmlem  32159  nodenselem8  32167  noetalem3  32191  nocvxmin  32220  scutun12  32243  funpartfun  32376  altopth1  32398  altopth2  32399  colineardim1  32494  lineext  32509  btwnconn1lem14  32533  brsegle  32541  hilbert1.2  32588  trer  32636  elicc3  32637  finminlem  32638  fneint  32669  fnessref  32678  refssfne  32679  neibastop1  32680  neibastop2lem  32681  neibastop2  32682  fnemeet2  32688  fnejoin2  32690  tailfb  32698  arg-ax  32737  ordtoplem  32756  onsuct0  32762  bj-gl4lem  32899  bj-nfimt  32937  bj-sngltag  33283  bj-restn0  33356  bj-0int  33368  bj-ismooredr2  33378  bj-bary1lem1  33480  icorempt2  33517  icoreresf  33518  relowlssretop  33529  finxpreclem6  33551  wl-ax8clv2  33696  fin2so  33711  poimirlem24  33748  poimirlem25  33749  poimirlem26  33750  poimirlem27  33751  poimirlem29  33753  poimirlem30  33754  poimirlem31  33755  mblfinlem1  33761  mblfinlem4  33764  ovoliunnfl  33766  itg2addnclem  33775  itg2addnclem2  33776  areacirc  33819  unirep  33821  filbcmb  33849  sdclem1  33852  fdc  33854  nninfnub  33860  isbnd2  33895  ssbnd  33900  prdsbnd2  33907  cntotbnd  33908  heibor1lem  33921  heiborlem1  33923  heiborlem4  33926  heiborlem6  33928  0idl  34137  intidl  34141  unichnidl  34143  keridl  34144  prnc  34179  iss2  34427  prtlem17  34657  prter2  34662  ax12indn  34724  lsatn0  34781  lsatcmp  34785  lssat  34798  lfl1  34852  lshpsmreu  34891  lkrin  34946  glbconxN  35160  cvrat4  35225  paddasslem17  35618  pmodlem2  35629  dalawlem14  35666  pclclN  35673  pclfinN  35682  pclfinclN  35732  poml4N  35735  osumcllem8N  35745  pexmidlem5N  35756  cdleme32a  36223  cdlemg33b0  36483  tendoeq2  36556  diaelrnN  36827  dihmeetlem1N  37072  dihglblem5apreN  37073  dihglblem2N  37076  dochvalr  37139  dochkrshp  37168  lcfl6  37282  lcfrvalsnN  37323  mapdordlem2  37419  mapdh8b  37562  mapdh9a  37571  hdmap14lem13  37662  eldioph2b  37829  eldiophss  37841  diophren  37880  ctbnfien  37885  rencldnfilem  37887  pellexlem3  37898  pellexlem5  37900  pellex  37902  pell14qrexpcl  37934  pellfundre  37948  pellfundge  37949  pellfundlb  37951  pellfundglb  37952  jm2.19lem4  38061  fnwe2lem2  38123  pwssplit4  38161  hbtlem5  38200  ss2iundf  38452  relexpmulg  38503  relexpxpmin  38510  relexpaddss  38511  dftrcl3  38513  dfrtrcl3  38526  clsk1indlem3  38842  isotone1  38847  isotone2  38848  ntrneiel2  38885  ntrneik4w  38899  onfrALT  39263  ax6e2ndeq  39274  snssiALT  39558  iinssf  39819  hirstL-ax3  41542  2reurex  41694  otiunsndisjX  41870  f1oresf1o2  41882  subsubelfzo0  41912  iccpartiltu  41934  iccpartigtl  41935  iccpartltu  41937  pfxccat3  42002  pfxccat3a  42005  reuccatpfxs1  42010  fmtnofac2lem  42056  fmtno4prmfac  42060  prmdvdsfmtnof1lem1  42072  lighneallem2  42099  opoeALTV  42170  opeoALTV  42171  even3prm2  42204  gbegt5  42225  gbowgt5  42226  sbgoldbwt  42241  sbgoldbst  42242  sbgoldbalt  42245  sbgoldbm  42248  mogoldbb  42249  sbgoldbo  42251  nnsum3primesle9  42258  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  wtgoldbnnsum4prm  42266  bgoldbnnsum3prm  42268  bgoldbtbndlem1  42269  bgoldbtbndlem4  42272  bgoldbtbnd  42273  upgrwlkupwlk  42290  sprsymrelf1lem  42310  sprsymrelfolem2  42312  sprsymrelf1  42315  sprsymrelfo  42316  mgmpropd  42344  copisnmnd  42378  mgm2mgm  42432  ringrng  42448  c0snmgmhm  42483  ztprmneprm  42694  mndpsuppss  42721  lindslinindimp2lem4  42819  lindslinindsimp2  42821  lindsrng01  42826  snlindsntor  42829  ldepspr  42831  isldepslvec2  42843  suppdm  42869  blen1b  42951  dignn0ldlem  42965  digexp  42970  nn0sumshdiglemB  42983  nn0sumshdiglem1  42984  iunord  42991  tfis2d  42996
  Copyright terms: Public domain W3C validator