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

Theorem syl5bi 220
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  |-  ( ph  <->  ps )
syl5bi.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bi  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 197 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 33 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr4g  273  ancomsd  455  3jao  1325  2euex  2343  2eu1  2352  eqneqall  2627  necon3bd  2632  necon2adOLD  2634  necon1adOLD  2637  pm2.61dne  2737  spcimgft  3157  rspc  3176  rspcimdv  3183  euind  3257  reuind  3275  sbciegft  3330  rspsbc  3378  ssexnelpss  3861  pwpw0  4148  sssn  4158  eqsn  4161  prel12  4177  prnebg  4182  pwsnALT  4214  intss1  4270  intmin  4275  uniintsn  4293  iinss  4350  disji2  4410  disjiun  4414  disjxiun  4420  disjss3  4422  trel3  4526  trin  4528  trintss  4534  eusvnfb  4620  reusv3  4632  copsexg  4706  otiunsndisj  4726  po3nr  4788  fri  4815  wefrc  4847  wereu2  4850  frsn  4924  ssrelrel  4954  relop  5004  iss  5171  restidsing  5180  poirr2  5243  xpcan  5292  xpcan2  5293  sossfld  5302  wfi  5432  wfis2fg  5436  onfr  5481  ord0eln0  5496  onmindif  5531  funopg  5633  funssres  5641  funun  5643  fv3  5894  fvmptt  5981  iinpreima  6025  fvn0ssdmfun  6028  dff3  6050  dff4  6051  fmptsng  6100  fmptsnd  6101  tpres  6132  fnprb  6138  fvclss  6162  isomin  6243  isofrlem  6246  weniso  6260  oprabid  6332  ssorduni  6626  onmindif2  6653  limuni3  6693  tfis2f  6696  tfinds  6700  tfinds2  6704  tfinds3  6705  funcnvuni  6760  f1oweALT  6791  f1o2ndf1  6915  poxp  6919  soxp  6920  fnse  6924  suppimacnv  6936  mpt2xopynvov0g  6971  reldmtpos  6992  rntpos  6997  wfrlem14  7060  wfrlem15  7061  onfununi  7071  smoiun  7091  tfrlem1  7105  tfr3  7128  frsucmptn  7167  tz7.49  7173  oaordi  7258  oawordeulem  7266  omeulem1  7294  oeordi  7299  oelimcl  7312  nnaordi  7330  nneob  7364  omsmolem  7365  erdisj  7422  qsss  7435  uniinqs  7454  map0g  7522  resixpfo  7571  ixpsnf1o  7573  xpdom3  7679  mapdom3  7753  phplem4  7763  php3  7767  unxpdomlem3  7787  ssfi  7801  findcard2  7820  findcard3  7823  frfi  7825  isfiniteg  7840  xpfi  7851  fiint  7857  finsschain  7890  dffi2  7946  marypha1lem  7956  marypha2  7962  supmo  7975  suplub2  7984  infmo  8020  ordiso2  8039  ordtypelem7  8048  ordtypelem8  8049  brwdom2  8097  unxpwdom2  8112  ixpiunwdom  8115  elirrv  8121  suc11reg  8133  noinfep  8173  cantnfle  8184  cantnflem1  8202  cantnf  8206  trcl  8220  epfrs  8223  rankpwi  8302  rankunb  8329  rankuni2b  8332  rankxplim3  8360  cplem1  8368  karden  8374  carddom2  8419  fseqenlem2  8463  ac10ct  8472  acni2  8484  acndom  8489  infpwfien  8500  alephordi  8512  alephord  8513  iunfictbso  8552  aceq3lem  8558  dfac5  8566  dfac2  8568  dfac12lem3  8582  dfac12r  8583  cdainflem  8628  cdainf  8629  cfub  8686  cfeq0  8693  coflim  8698  cfslb2n  8705  cofsmo  8706  coftr  8710  infpssr  8745  fin23lem7  8753  fin23lem11  8754  fin23lem21  8776  isf32lem2  8791  isf34lem4  8814  isfin1-2  8822  isfin1-3  8823  fin1a2lem9  8845  fin1a2lem11  8847  fin1a2lem12  8848  fin1a2lem13  8849  domtriomlem  8879  axdc3lem2  8888  axcclem  8894  ac6c4  8918  zorn2lem4  8936  zorn2lem5  8937  zorn2lem7  8939  ttukeylem5  8950  ttukeyg  8954  brdom6disj  8967  fnrndomg  8970  iunfo  8971  iundom2g  8972  ficard  8997  konigthlem  9000  alephval2  9004  pwcfsdom  9015  fpwwe2lem9  9070  fpwwe2lem11  9072  fpwwe2lem12  9073  fpwwe2lem13  9074  pwfseqlem3  9092  gchpwdom  9102  winalim2  9128  gchina  9131  wunex2  9170  tskr1om2  9200  tskxpss  9204  inar1  9207  tskuni  9215  gruun  9238  grudomon  9249  grur1  9252  ltmpi  9336  ltexprlem2  9469  ltexprlem6  9473  reclem2pr  9480  reclem3pr  9481  reclem4pr  9482  suplem1pr  9484  mulgt0sr  9536  supsrlem  9542  axrrecex  9594  axpre-sup  9600  ltlen  9742  negn0  10055  negf1o  10056  mulge0b  10482  supaddc  10581  supadd  10582  supmul1  10583  supmullem1  10584  supmullem2  10585  supmul  10586  infmrclOLD  10600  cju  10612  nnsub  10655  0mnnnnn0  10909  un0addcl  10910  un0mulcl  10911  nn0sub  10927  nn0n0n1ge2b  10940  peano5uzi  11031  eluzuzle  11174  zsupss  11260  qbtwnre  11499  xrsupexmnf  11597  xrinfmexpnf  11598  xrsupsslem  11599  xrinfmsslem  11600  xrub  11604  supxrun  11608  xrinfm0OLD  11634  ixxdisj  11657  icodisj  11764  difreicc  11771  uzsubsubfz  11828  elfzmlbp  11909  fzofzim  11969  elfznelfzo  12020  injresinj  12031  flval3  12056  modirr  12166  ssnn0fi  12203  seqf1o  12260  expcl2lem  12290  expnegz  12312  expaddz  12322  expmulz  12324  facwordi  12480  faclbnd4lem4  12487  bccl  12513  hashnfinnn0  12548  hashgt12el  12599  hashgt12el2  12600  hashfun  12613  hashbclem  12619  hashbc  12620  hashfacen  12621  hashf1lem1  12622  hashf1  12624  hash2pwpr  12639  fi1uzind  12654  brfi1indALT  12657  wrdind  12835  wrd2ind  12836  reuccats1  12839  swrdccatin1  12841  swrdccatin2  12845  swrdccat3  12850  swrdccat3blem  12853  cshw1  12923  cshwcsh2id  12929  wwlktovfo  13033  rtrclreclem3  13123  dfrtrcl2  13125  sqrlem1  13306  sqrlem6  13311  rexanre  13409  cau3lem  13417  2clim  13635  summo  13782  fsum2dlem  13830  fsumiun  13880  prodmo  13989  fprod2dlem  14033  bpolycl  14104  rpnnen2  14277  odd2np1lem  14363  bitsfzo  14408  sadcaddlem  14430  gcd0id  14486  algcvgblem  14535  lcmfunsnlem1  14609  lcmfunsnlem2lem1  14610  lcmfunsnlem2  14612  prmdvdsexpr  14668  prmfac1  14670  coprmproddvdslem  14678  qnumdencl  14687  hashdvds  14722  pcneg  14822  prmpwdvds  14847  prmreclem2  14860  4sqlem12  14899  vdwlem6  14935  vdwlem10  14939  vdwlem13  14942  0ram  14977  ram0  14979  ramz  14982  ramcl  14986  prmgaplem3  15022  prmgaplem4  15023  prmgaplem5  15024  prmgaplem6  15025  cshwshashlem1  15065  prmlem0  15076  firest  15330  imasaddfnlem  15433  imasvscafn  15442  mremre  15509  cicsym  15708  initoid  15899  termoid  15900  iszeroi  15903  drsdirfi  16182  pospo  16218  joinfval  16246  meetfval  16260  lubun  16368  odupos  16380  acsfiindd  16422  psss  16459  mnd1id  16578  symgfix2  17056  f1omvdco2  17088  symggen  17110  odcau  17255  pgpfi  17256  sylow2blem3  17273  sylow3lem2  17279  lsmmod  17324  efgsfo  17388  frgpuptinv  17420  frgpnabllem1  17508  cyggeninv  17517  lt6abl  17528  cyggex2  17530  gsumval3lem2  17539  gsumval3  17540  gsum2d2  17605  dmdprdd  17630  dprd2da  17674  pgpfac1lem5  17711  pgpfac  17716  srgbinomlem4  17775  dvdsrtr  17879  dvdsrmul1  17880  lss1d  18185  lspsolvlem  18364  lspsnat  18367  lbsextlem2  18381  lbsextlem3  18382  0ring  18493  01eq0ring  18495  0ring01eqbi  18496  rng1nfld  18501  domnmuln0  18521  abvn0b  18525  mvrf1  18648  mplcoe5lem  18690  opsrtoslem2  18707  cply1mul  18886  coe1fzgsumdlem  18894  gsummoncoe1  18897  pf1ind  18942  evl1gsumdlem  18943  xrsdsreclblem  19013  qsssubdrg  19026  prmirredlem  19062  cygznlem3  19138  obslbs  19291  dsmmacl  19302  lindfrn  19377  lmiclbs  19393  lmisfree  19398  matecl  19448  mat1dimelbas  19494  scmateALT  19535  mdetdiaglem  19621  mdet0  19629  mdetunilem9  19643  gsummatr01  19682  cpmatmcllem  19740  m2cpminvid2lem  19776  pmatcollpw3fi1lem2  19809  chfacfscmul0  19880  chfacfpmmul0  19884  cayhamlem3  19909  unitgOLD  19981  tgcl  19983  tgidm  19994  indistopon  20014  fctop  20017  cctop  20019  ppttop  20020  pptbas  20021  epttop  20022  opnnei  20134  neiptopnei  20146  tgrest  20173  restntr  20196  perfopn  20199  ordtrest2lem  20217  isreg2  20391  lmmo  20394  ordthauslem  20397  cmpsublem  20412  cmpsub  20413  cmpcld  20415  hauscmplem  20419  iunconlem  20440  uncon  20442  2ndcrest  20467  2ndcctbss  20468  2ndcdisj  20469  dis2ndc  20473  locfincmp  20539  comppfsc  20545  txbas  20580  ptbasin  20590  ptbasfi  20594  txcls  20617  txbasval  20619  ptpjopn  20625  ptclsg  20628  dfac14lem  20630  xkoccn  20632  txcnp  20633  txindis  20647  txdis1cn  20648  tx1stc  20663  tx2ndc  20664  txkgen  20665  xkoco1cn  20670  xkoco2cn  20671  xkococn  20673  xkoinjcn  20700  txcon  20702  fbfinnfr  20854  opnfbas  20855  filtop  20868  isfild  20871  fbunfip  20882  filcon  20896  fbasrn  20897  filuni  20898  isufil2  20921  filssufilg  20924  ufileu  20932  filufint  20933  rnelfmlem  20965  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem4  20970  fmfnfm  20971  hausflimi  20993  hauspwpwf1  21000  flffbas  21008  flftg  21009  alexsublem  21057  alexsubALTlem1  21060  alexsubALTlem2  21061  alexsubALTlem3  21062  alexsubALTlem4  21063  alexsubALT  21064  ptcmplem3  21067  cldsubg  21123  qustgpopn  21132  tgptsmscld  21163  tsmsxplem1  21165  ustfilxp  21225  imasdsf1olem  21386  bldisj  21411  xbln0  21427  prdsxmslem2  21542  xrsblre  21827  icccmplem2  21839  reconn  21844  opnreen  21847  xrge0tsms  21850  metdsre  21868  metdsreOLD  21883  iccpnfcnv  21970  cnheiborlem  21980  phtpc01  22025  pi1blem  22068  tchcph  22209  cfilfcls  22242  iscau4  22247  bcthlem5  22294  bcth3  22297  hlhil  22395  ovolctb  22441  ovoliunlem2  22454  ovoliunnul  22458  ovolicc2  22474  volfiniun  22498  iundisj  22499  dyadmax  22554  dyadmbllem  22555  vitalilem2  22565  ismbfd  22594  mbfimaopnlem  22609  itg11  22647  i1faddlem  22649  mbfi1fseqlem4  22674  bddmulibl  22794  limciun  22847  perfdvf  22856  rolle  22940  dvivthlem1  22958  dvne0  22961  lhop1  22964  lhop2  22965  itgsubst  22999  dvdsq1p  23109  fta1g  23116  dgrco  23227  plydivex  23248  fta1  23259  ulmcaulem  23347  abelthlem2  23385  pilem2  23405  pilem2OLD  23406  cxpmul2z  23634  cxpcn3lem  23685  xrlimcnp  23892  jensen  23912  wilthlem2  23992  wilthlem3  23993  muval2  24059  sqf11  24064  ppiublem1  24128  fsumvma  24139  lgsdir2lem2  24250  lgsdir2lem5  24253  dchrisum0fno1  24347  pntlem3  24445  pntleml  24447  ostthlem1  24463  ostth2lem2  24470  colinearalg  24938  axcontlem2  24993  axcontlem8  24999  usgrares1  25136  nbgraf1olem5  25171  cusgrarn  25185  nbcusgra  25189  uvtxnbgra  25219  wlkcpr  25255  3v3e3cycl2  25390  usg2wlkeq  25434  wlkiswwlksur  25445  clwlkswlks  25484  clwlkisclwwlklem2a4  25510  clwlkisclwwlklem1  25513  clwwlkf1  25522  erclwwlktr  25541  erclwwlkntr  25553  hashecclwwlkn1  25560  usghashecclwwlk  25561  wlklenvclwlk  25565  clwlkfoclwwlk  25571  vdusgra0nedg  25634  nbhashuvtx  25642  usgravd0nedg  25644  usgravd00  25645  rusgranumwlklem1  25675  3cyclfrgrarn1  25738  frgranbnb  25746  frgrancvvdeqlem3  25758  frgrancvvdeqlem4  25759  frgrancvvdeqlemC  25765  frgrawopreglem3  25772  frgrawopreglem5  25774  frgrawopreg2  25777  2spotiundisj  25788  2spotmdisj  25794  extwwlkfablem2  25804  numclwwlkun  25805  numclwwlkovf2ex  25812  numclwlk1lem2f1  25820  gxnn0neg  25989  gxnn0suc  25990  lnon0  26437  shmodsi  27040  shlub  27065  spanunsni  27230  h1datomi  27232  stm1ri  27895  stadd3i  27899  mdsl1i  27972  cvmdi  27975  superpos  28005  chjatom  28008  chirredi  28045  atcvat4i  28048  sumdmdii  28066  sumdmdlem  28069  cdj3lem2a  28087  cdj3lem3a  28090  cdj3i  28092  disji2f  28189  disjif2  28193  iundisjf  28201  rnmpt2ss  28278  xrge0infssOLD  28347  iundisjfi  28378  nn0min  28391  xrge0tsmsd  28556  cnre2csqima  28725  ordtrest2NEWlem  28736  xrge0iifcnv  28747  lmxrge0  28766  measdivcstOLD  29054  dya2iocuni  29113  omssubadd  29136  omssubaddOLD  29140  eulerpartlems  29201  bnj849  29744  bnj1118  29801  derangenlem  29902  erdszelem9  29930  pconcon  29962  iccllyscon  29981  cvmsval  29997  cvmscld  30004  cvmsss2  30005  cvmopnlem  30009  cvmfolem  30010  cvmliftmolem2  30013  cvmlift2lem10  30043  cvmlift2lem12  30045  cvmlift3lem5  30054  cvmlift3lem8  30057  msubvrs  30206  mthmblem  30226  untsucf  30345  3orel1  30350  3orel2  30351  3orel3  30352  nepss  30358  dfon2lem5  30440  dfon2lem6  30441  dfon2lem7  30442  dfon2lem8  30443  rdgprc  30448  trpredtr  30478  dftrpred3g  30481  trpredrec  30486  frmin  30487  frind  30488  frins2fg  30492  wsuclem  30515  frrlem5e  30529  nodenselem4  30578  nodenselem8  30582  nocvxmin  30585  nofulllem5  30600  funpartfun  30715  altopth1  30737  altopth2  30738  colineardim1  30833  lineext  30848  btwnconn1lem14  30872  brsegle  30880  hilbert1.2  30927  trer  30977  elicc3  30978  finminlem  30979  fneint  31009  fnessref  31018  refssfne  31019  neibastop1  31020  neibastop2lem  31021  neibastop2  31022  fnemeet2  31028  fnejoin2  31030  tailfb  31038  arg-ax  31081  ordtoplem  31100  onsuct0  31106  bj-gl4lem  31182  bj-sngltag  31545  bj-bary1lem1  31680  icorempt2  31718  icoreresf  31719  relowlssretop  31730  finxpreclem6  31752  fin2so  31896  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  mblfinlem1  31941  mblfinlem4  31944  ovoliunnfl  31946  itg2addnclem  31957  itg2addnclem2  31958  areacirc  32001  unirep  32003  filbcmb  32031  fzadd2  32034  sdclem1  32036  fdc  32038  nninfnub  32044  isbnd2  32079  ssbnd  32084  prdsbnd2  32091  cntotbnd  32092  heibor1lem  32105  heiborlem1  32107  heiborlem4  32110  heiborlem6  32112  0idl  32222  intidl  32226  unichnidl  32228  keridl  32229  prnc  32264  ceqsex3OLD  32400  prtlem17  32416  prter2  32421  ax12indn  32483  lsatn0  32534  lsatcmp  32538  lssat  32551  lfl1  32605  lshpsmreu  32644  lkrin  32699  glbconxN  32912  cvrat4  32977  paddasslem17  33370  pmodlem2  33381  dalawlem14  33418  pclclN  33425  pclfinN  33434  pclfinclN  33484  poml4N  33487  osumcllem8N  33497  pexmidlem5N  33508  cdleme32a  33977  cdlemg33b0  34237  tendoeq2  34310  diaelrnN  34582  dihmeetlem1N  34827  dihglblem5apreN  34828  dihglblem2N  34831  dochvalr  34894  dochkrshp  34923  lcfl6  35037  lcfrvalsnN  35078  mapdordlem2  35174  mapdh8b  35317  mapdh9a  35327  hdmap14lem13  35420  eldioph2b  35574  eldiophss  35586  diophren  35625  ctbnfien  35630  rencldnfilem  35632  pellexlem3  35645  pellexlem5  35647  pellex  35649  pell14qrexpcl  35683  pellfundre  35699  pellfundge  35700  pellfundlb  35702  pellfundglb  35703  jm2.19lem4  35817  fnwe2lem2  35879  pwssplit4  35917  hbtlem5  35957  ss2iundf  36221  relexpmulg  36272  relexpxpmin  36279  relexpaddss  36280  dftrcl3  36282  dfrtrcl3  36295  isprm7  36630  onfrALT  36885  ax6e2ndeq  36896  snssiALT  37197  hirstL-ax3  38350  2reurex  38473  iccpartiltu  38606  iccpartigtl  38607  iccpartltu  38609  opoeALTV  38682  opeoALTV  38683  gbegt5  38732  gbogt5  38733  bgoldbwt  38748  bgoldbst  38749  sgoldbalt  38752  nnsum3primesle9  38759  evengpoap3  38764  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  wtgoldbnnsum4prm  38767  bgoldbnnsum3prm  38769  bgoldbtbndlem1  38770  bgoldbtbndlem4  38773  bgoldbtbnd  38774  pfxccat3  38837  pfxccat3a  38840  reuccatpfxs1  38845  elnelall  38850  ralnralall  38853  propeqop  38865  iunopeqop  38870  otiunsndisjX  38871  fundmge2nop  38889  subsubelfzo0  38916  edgumgra  39042  ausgrumgri  39048  ausgrusgri  39049  usgredgedga  39090  uhgr0v0e  39095  uhgrspan1  39144  fusgrfisstep  39161  nbuhgr  39177  nbgr2vtx1edg  39182  nbuhgr2vtx1edgb  39184  uhgrnbgr0nb  39186  edgnbusgreu  39205  nbusgredgeu0  39206  nbusgrf1o0  39207  cusgredg  39248  cplgr1v  39253  cusgrfi  39275  usgredgsscusgredg  39276  usgra2pthspth  39284  usgvincvad  39335  usgvincvadALT  39338  usgedgvadf1lem2  39345  usgedgvadf1ALTlem2  39348  usgfis  39377  usgfisALT  39381  mgmpropd  39394  copisnmnd  39428  mgm2mgm  39482  ringrng  39498  c0snmgmhm  39533  ztprmneprm  39749  mndpsuppss  39777  lindslinindimp2lem4  39875  lindslinindsimp2  39877  lindsrng01  39882  snlindsntor  39885  ldepspr  39887  isldepslvec2  39899  suppdm  39925  blen1b  40020  dignn0ldlem  40034  digexp  40039  nn0sumshdiglemB  40052  nn0sumshdiglem1  40053
  Copyright terms: Public domain W3C validator