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

Theorem syl5bi 217
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 194 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr4g  270  ancomsd  454  3jao  1289  ax12indn  2266  2euex  2375  2eu1  2386  eqneqall  2674  necon3bd  2679  necon2adOLD  2681  necon1adOLD  2684  pm2.61dne  2784  spcimgft  3189  rspc  3208  rspcimdv  3215  euind  3290  reuind  3307  sbciegft  3362  rspsbc  3421  pwpw0  4175  sssn  4185  eqsn  4188  prel12  4203  prnebg  4208  pwsnALT  4240  intss1  4297  intmin  4302  uniintsn  4319  iinss  4376  disji2  4434  disjiun  4437  disjxiun  4444  disjss3  4446  trel3  4548  trin  4550  trintss  4556  eusvnfb  4643  reusv3  4655  copsexg  4732  copsexgOLD  4733  otiunsndisj  4753  po3nr  4814  fri  4841  wefrc  4873  wereu2  4876  onfr  4917  ord0eln0  4932  onmindif  4967  frsn  5069  ssrelrel  5101  relop  5151  iss  5319  restidsing  5328  poirr2  5389  xpcan  5441  xpcan2  5442  sossfld  5452  funopg  5618  funssres  5626  funun  5628  fv3  5877  fvmptt  5963  iinpreima  6009  suppssOLD  6012  dff3  6032  dff4  6033  fmptsng  6080  fmptsnd  6081  fnprb  6117  fnprOLD  6118  fvclss  6140  isomin  6219  isofrlem  6222  weniso  6236  oprabid  6306  ssorduni  6599  onmindif2  6625  limuni3  6665  tfis2f  6668  tfinds  6672  tfinds2  6676  tfinds3  6677  funcnvuni  6734  f1oweALT  6765  f1o2ndf1  6888  poxp  6892  soxp  6893  fnse  6897  suppimacnv  6909  mpt2xopynvov0g  6939  reldmtpos  6960  rntpos  6965  onfununi  7009  smoiun  7029  tfrlem1  7042  tfr3  7065  frsucmptn  7101  tz7.49  7107  oaordi  7192  oawordeulem  7200  omeulem1  7228  oeordi  7233  oelimcl  7246  nnaordi  7264  nneob  7298  omsmolem  7299  erdisj  7356  qsss  7369  uniinqs  7388  map0g  7455  resixpfo  7504  ixpsnf1o  7506  xpdom3  7612  mapdom3  7686  phplem4  7696  php3  7700  unxpdomlem3  7723  ssfi  7737  findcard2  7756  findcard3  7759  frfi  7761  isfiniteg  7776  xpfi  7787  fiint  7793  finsschain  7823  dffi2  7879  marypha1lem  7889  marypha2  7895  supmo  7908  suplub2  7917  ordiso2  7936  ordtypelem7  7945  ordtypelem8  7946  brwdom2  7995  unxpwdom2  8010  ixpiunwdom  8013  elirrv  8019  suc11reg  8032  noinfep  8072  cantnfle  8086  cantnflem1  8104  cantnf  8108  cantnfleOLD  8116  cantnflem1OLD  8127  cantnfOLD  8130  trcl  8155  epfrs  8158  rankpwi  8237  rankunb  8264  rankuni2b  8267  rankxplim3  8295  cplem1  8303  karden  8309  carddom2  8354  fseqenlem2  8402  ac10ct  8411  acni2  8423  acndom  8428  infpwfien  8439  alephordi  8451  alephord  8452  iunfictbso  8491  aceq3lem  8497  dfac5  8505  dfac2  8507  dfac12lem3  8521  dfac12r  8522  cdainflem  8567  cdainf  8568  cfub  8625  cfeq0  8632  coflim  8637  cfslb2n  8644  cofsmo  8645  coftr  8649  infpssr  8684  fin23lem7  8692  fin23lem11  8693  fin23lem21  8715  isf32lem2  8730  isf34lem4  8753  isfin1-2  8761  isfin1-3  8762  fin1a2lem9  8784  fin1a2lem11  8786  fin1a2lem12  8787  fin1a2lem13  8788  domtriomlem  8818  axdc3lem2  8827  axcclem  8833  ac6c4  8857  zorn2lem4  8875  zorn2lem5  8876  zorn2lem7  8878  ttukeylem5  8889  ttukeyg  8893  brdom6disj  8906  fnrndomg  8909  iunfo  8910  iundom2g  8911  ficard  8936  konigthlem  8939  alephval2  8943  pwcfsdom  8954  fpwwe2lem9  9012  fpwwe2lem11  9014  fpwwe2lem12  9015  fpwwe2lem13  9016  pwfseqlem3  9034  gchpwdom  9044  winalim2  9070  gchina  9073  wunex2  9112  tskr1om2  9142  tskxpss  9146  inar1  9149  tskuni  9157  gruun  9180  grudomon  9191  grur1  9194  ltmpi  9278  ltexprlem2  9411  ltexprlem6  9415  reclem2pr  9422  reclem3pr  9423  reclem4pr  9424  suplem1pr  9426  mulgt0sr  9478  supsrlem  9484  axrrecex  9536  axpre-sup  9542  ltlen  9682  mulge0b  10408  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  infmrcl  10518  cju  10528  nnsub  10570  0mnnnnn0  10824  un0addcl  10825  un0mulcl  10826  nn0sub  10842  nn0n0n1ge2b  10856  peano5uzi  10945  eluzuzle  11086  negn0  11164  zsupss  11167  qbtwnre  11394  xrsupexmnf  11492  xrinfmexpnf  11493  xrsupsslem  11494  xrinfmsslem  11495  xrub  11499  supxrun  11503  xrinfm0  11524  ixxdisj  11540  icodisj  11641  difreicc  11648  uzsubsubfz  11703  elfzmlbp  11779  fzofzim  11833  elfznelfzo  11879  injresinj  11890  flval3  11914  modirr  12020  ssnn0fi  12057  seqf1o  12111  expcl2lem  12141  expnegz  12162  expaddz  12172  expmulz  12174  facwordi  12329  faclbnd4lem4  12336  bccl  12362  hashnfinnn0  12394  hashgt12el  12440  hashgt12el2  12441  hashfun  12455  hashbclem  12461  hashbc  12462  hashfacen  12463  hashf1lem1  12464  hashf1  12466  hash2pwpr  12479  brfi1uzind  12492  wrdind  12659  wrd2ind  12660  reuccats1  12663  swrdccatin1  12665  swrdccatin2  12669  swrdccat3  12674  swrdccat3blem  12677  cshw1  12747  cshwcsh2id  12753  wwlktovfo  12853  sqrlem1  13033  sqrlem6  13038  rexanre  13135  cau3lem  13143  2clim  13351  summo  13495  fsum2dlem  13541  fsumiun  13591  rpnnen2  13813  odd2np1lem  13897  bitsfzo  13937  sadcaddlem  13959  gcd0id  14013  algcvgblem  14058  prmdvdsexpr  14109  prmfac1  14111  qnumdencl  14124  hashdvds  14157  pcneg  14249  prmpwdvds  14274  prmreclem2  14287  4sqlem12  14326  vdwlem6  14356  vdwlem10  14360  vdwlem13  14363  0ram  14390  ram0  14392  ramz  14395  ramcl  14399  cshwshashlem1  14431  prmlem0  14442  firest  14681  imasaddfnlem  14776  imasvscafn  14785  mremre  14852  drsdirfi  15418  pospo  15453  joinfval  15481  meetfval  15495  lubun  15603  odupos  15615  acsfiindd  15657  psss  15694  symgfix2  16233  f1omvdco2  16266  symggen  16288  odcau  16417  pgpfi  16418  sylow2blem3  16435  sylow3lem2  16441  lsmmod  16486  efgsfo  16550  frgpuptinv  16582  frgpnabllem1  16665  cyggeninv  16674  lt6abl  16685  cyggex2  16687  gsumval3OLD  16696  gsumval3lem2  16698  gsumval3  16699  gsum2d2  16790  dmdprdd  16818  dprd2da  16878  pgpfac1lem5  16917  pgpfac  16922  srgbinomlem4  16979  dvdsrtr  17082  dvdsrmul1  17083  lss1d  17389  lspsolvlem  17568  lspsnat  17571  lbsextlem2  17585  lbsextlem3  17586  domnmuln0  17715  abvn0b  17719  mvrf1  17849  mplcoe5lem  17898  opsrtoslem2  17917  cply1mul  18103  coe1fzgsumdlem  18111  gsummoncoe1  18114  pf1ind  18159  evl1gsumdlem  18160  xrsdsreclblem  18229  qsssubdrg  18242  prmirredlem  18287  prmirredlemOLD  18290  cygznlem3  18372  obslbs  18525  dsmmacl  18536  lindfrn  18620  lmiclbs  18636  lmisfree  18641  matecl  18691  mat1dimelbas  18737  scmateALT  18778  mdetdiaglem  18864  mdet0  18872  mdetunilem9  18886  gsummatr01  18925  cpmatmcllem  18983  m2cpminvid2lem  19019  pmatcollpw3fi1lem2  19052  chfacfscmul0  19123  chfacfpmmul0  19127  cayhamlem3  19152  unitg  19232  tgcl  19234  tgidm  19245  indistopon  19265  fctop  19268  cctop  19270  ppttop  19271  pptbas  19272  epttop  19273  opnnei  19384  neiptopnei  19396  tgrest  19423  restntr  19446  perfopn  19449  ordtrest2lem  19467  isreg2  19641  lmmo  19644  ordthauslem  19647  cmpsublem  19662  cmpsub  19663  cmpcld  19665  hauscmplem  19669  bwthOLD  19674  iunconlem  19691  uncon  19693  2ndcrest  19718  2ndcctbss  19719  2ndcdisj  19720  dis2ndc  19724  txbas  19800  ptbasin  19810  ptbasfi  19814  txcls  19837  txbasval  19839  ptpjopn  19845  ptclsg  19848  dfac14lem  19850  xkoccn  19852  txcnp  19853  txindis  19867  txdis1cn  19868  tx1stc  19883  tx2ndc  19884  txkgen  19885  xkoco1cn  19890  xkoco2cn  19891  xkococn  19893  xkoinjcn  19920  txcon  19922  fbfinnfr  20074  opnfbas  20075  filtop  20088  isfild  20091  fbunfip  20102  filcon  20116  fbasrn  20117  filuni  20118  isufil2  20141  filssufilg  20144  ufileu  20152  filufint  20153  rnelfmlem  20185  rnelfm  20186  fmfnfmlem2  20188  fmfnfmlem4  20190  fmfnfm  20191  hausflimi  20213  hauspwpwf1  20220  flffbas  20228  flftg  20229  alexsublem  20276  alexsubALTlem1  20279  alexsubALTlem2  20280  alexsubALTlem3  20281  alexsubALTlem4  20282  alexsubALT  20283  ptcmplem3  20286  cldsubg  20341  divstgpopn  20350  tgptsmscld  20385  tsmsxplem1  20387  ustfilxp  20447  imasdsf1olem  20608  bldisj  20633  xbln0  20649  prdsxmslem2  20764  xrsblre  21048  icccmplem2  21060  reconn  21065  opnreen  21068  xrge0tsms  21071  metdsre  21089  iccpnfcnv  21176  cnheiborlem  21186  phtpc01  21228  pi1blem  21271  tchcph  21412  cfilfcls  21445  iscau4  21450  bcthlem5  21499  bcth3  21502  hlhil  21590  ovolctb  21633  ovoliunlem2  21646  ovoliunnul  21650  ovolicc2  21665  volfiniun  21689  iundisj  21690  dyadmax  21739  dyadmbllem  21740  vitalilem2  21750  ismbfd  21779  mbfimaopnlem  21794  itg11  21830  i1faddlem  21832  mbfi1fseqlem4  21857  bddmulibl  21977  limciun  22030  perfdvf  22039  rolle  22123  dvivthlem1  22141  dvne0  22144  lhop1  22147  lhop2  22148  itgsubst  22182  dvdsq1p  22293  fta1g  22300  dgrco  22403  plydivex  22424  fta1  22435  ulmcaulem  22520  abelthlem2  22558  pilem2  22578  cxpmul2z  22797  cxpcn3lem  22846  xrlimcnp  23023  jensen  23043  wilthlem2  23068  wilthlem3  23069  muval2  23133  sqf11  23138  ppiublem1  23202  fsumvma  23213  lgsdir2lem2  23324  lgsdir2lem5  23327  dchrisum0fno1  23421  pntlem3  23519  pntleml  23521  ostthlem1  23537  ostth2lem2  23544  colinearalg  23886  axcontlem2  23941  axcontlem8  23947  usgra2edg  24055  usgrares1  24083  nbgraf1olem5  24118  cusgrarn  24132  nbcusgra  24136  uvtxnbgra  24166  wlkcpr  24202  3v3e3cycl2  24337  usg2wlkeq  24381  wlkiswwlksur  24392  clwlkswlks  24431  clwlkisclwwlklem2a4  24457  clwlkisclwwlklem1  24460  clwwlkf1  24469  erclwwlktr  24488  erclwwlkntr  24500  hashecclwwlkn1  24507  usghashecclwwlk  24508  wlklenvclwlk  24512  clwlkfoclwwlk  24518  vdusgra0nedg  24581  nbhashuvtx  24589  usgravd0nedg  24591  usgravd00  24592  rusgranumwlklem1  24622  3cyclfrgrarn1  24685  frgranbnb  24693  frgrancvvdeqlem3  24706  frgrancvvdeqlem4  24707  frgrancvvdeqlemC  24713  frgrawopreglem3  24720  frgrawopreglem4  24721  frgrawopreglem5  24722  frgrawopreg2  24725  2spotiundisj  24736  2spotmdisj  24742  extwwlkfablem2  24752  numclwwlkun  24753  numclwwlkovf2ex  24760  numclwlk1lem2f1  24768  gxnn0neg  24938  gxnn0suc  24939  lnon0  25386  shmodsi  25980  shlub  26005  spanunsni  26170  h1datomi  26172  stm1ri  26836  stadd3i  26840  mdsl1i  26913  cvmdi  26916  superpos  26946  chjatom  26949  chirredi  26986  atcvat4i  26989  sumdmdii  27007  sumdmdlem  27010  cdj3lem2a  27028  cdj3lem3a  27031  cdj3i  27033  disji2f  27108  disjif2  27112  iundisjf  27118  rnmpt2ss  27184  suppss3  27219  xrge0infss  27245  iundisjfi  27266  nn0min  27276  xrge0tsmsd  27435  cnre2csqima  27526  ordtrest2NEWlem  27537  xrge0iifcnv  27548  lmxrge0  27567  measdivcstOLD  27832  dya2iocuni  27891  eulerpartlems  27936  derangenlem  28252  erdszelem9  28280  pconcon  28313  iccllyscon  28332  cvmsval  28348  cvmscld  28355  cvmsss2  28356  cvmopnlem  28360  cvmfolem  28361  cvmliftmolem2  28364  cvmlift2lem10  28394  cvmlift2lem12  28396  cvmlift3lem5  28405  cvmlift3lem8  28408  rtrclreclem.trans  28541  dfrtrcl2  28543  untsucf  28554  3orel1  28559  3orel2  28560  3orel3  28561  nepss  28567  prodmo  28642  fprod2dlem  28684  dfon2lem5  28793  dfon2lem6  28794  dfon2lem7  28795  dfon2lem8  28796  rdgprc  28801  wfi  28861  wfis2fg  28865  trpredtr  28887  dftrpred3g  28890  trpredrec  28895  frmin  28896  frind  28897  frins2fg  28901  wfrlem14  28930  wfrlem15  28931  wsuclem  28955  frrlem5e  28969  nodenselem4  29018  nodenselem8  29022  nocvxmin  29025  nofulllem5  29040  funpartfun  29167  altopth1  29189  altopth2  29190  colineardim1  29285  lineext  29300  btwnconn1lem14  29324  brsegle  29332  hilbert1.2  29379  bpolycl  29388  arg-ax  29455  ordtoplem  29474  onsuct0  29480  fin2so  29614  supaddc  29615  supadd  29616  mblfinlem1  29626  mblfinlem4  29629  ovoliunnfl  29631  itg2addnclem  29641  itg2addnclem2  29642  areacirc  29687  trer  29709  elicc3  29710  finminlem  29711  fneint  29747  fnessref  29763  refssfne  29764  locfincmp  29774  comppfsc  29777  neibastop1  29778  neibastop2lem  29779  neibastop2  29780  fnemeet2  29786  fnejoin2  29788  tailfb  29796  unirep  29804  filbcmb  29832  fzadd2  29835  sdclem1  29837  fdc  29839  nninfnub  29845  isbnd2  29880  ssbnd  29885  prdsbnd2  29892  cntotbnd  29893  heibor1lem  29906  heiborlem1  29908  heiborlem4  29911  heiborlem6  29913  0idl  30023  intidl  30027  unichnidl  30029  keridl  30030  prnc  30065  ceqsex3OLD  30203  prtlem17  30219  prter2  30224  eldioph2b  30298  eldiophss  30310  diophren  30349  ctbnfien  30354  rencldnfilem  30356  pellexlem3  30369  pellexlem5  30371  pellex  30373  pell14qrexpcl  30405  pellfundre  30419  pellfundge  30420  pellfundlb  30422  pellfundglb  30423  jm2.19lem4  30538  fnwe2lem2  30601  pwssplit4  30639  hbtlem5  30681  isprm7  30795  hirstL-ax3  31554  2reurex  31653  elnelall  31760  ralnralall  31761  otiunsndisjX  31768  subsubelfzo0  31807  usgra2pthspth  31820  usgvincvad  31873  usgvincvadALT  31876  usgedgvadf1lem2  31883  usgedgvadf1ALTlem2  31886  usgfis  31915  usgfisALT  31919  iopmapxp  31960  mgm2mgm  31977  ringrng0  31982  ztprmneprm  32000  0rng  32028  01eq0rng  32030  mndpsuppss  32037  lindslinindimp2lem4  32135  lindslinindsimp2  32137  lindsrng01  32142  snlindsntor  32145  ldepspr  32147  isldepslvec2  32159  rng1nfld  32167  onfrALT  32401  ax6e2ndeq  32412  snssiALT  32708  bnj849  33062  bnj1118  33119  bj-gl4lem  33265  bj-sngltag  33622  bj-bary1lem1  33752  lsatn0  33796  lsatcmp  33800  lssat  33813  lfl1  33867  lshpsmreu  33906  lkrin  33961  glbconxN  34174  cvrat4  34239  paddasslem17  34632  pmodlem2  34643  dalawlem14  34680  pclclN  34687  pclfinN  34696  pclfinclN  34746  poml4N  34749  osumcllem8N  34759  pexmidlem5N  34770  cdleme32a  35237  cdlemg33b0  35497  tendoeq2  35570  diaelrnN  35842  dihmeetlem1N  36087  dihglblem5apreN  36088  dihglblem2N  36091  dochvalr  36154  dochkrshp  36183  lcfl6  36297  lcfrvalsnN  36338  mapdordlem2  36434  mapdh8b  36577  mapdh9a  36587  hdmap14lem13  36680
  Copyright terms: Public domain W3C validator