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

Theorem syl5bi 209
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-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 187 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4g  262  ancomsd  441  3jao  1245  sbequ2OLD  1661  19.9htOLD  1803  19.9tOLD  1880  ax12olem5OLD  2015  ax11indn  2272  2euex  2353  necon3bd  2636  necon2ad  2647  necon1ad  2666  pm2.61dne  2676  spcimgft  3020  rspc  3039  rspcimdv  3046  euind  3114  reuind  3130  sbciegft  3184  rspsbc  3232  pwpw0  3939  sssn  3950  eqsn  3953  prel12  3968  prnebg  3972  pwsnALT  4003  intss1  4058  intmin  4063  uniintsn  4080  iinss  4135  disji2  4192  disjiun  4195  disjxiun  4202  disjss3  4204  trel3  4303  trin  4305  trintss  4311  copsexg  4435  po3nr  4510  fri  4537  wefrc  4569  wereu2  4572  onfr  4613  ord0eln0  4628  onmindif  4664  eusvnfb  4712  reusv3  4724  ssorduni  4759  onmindif2  4785  limuni3  4825  tfis2f  4828  tfinds  4832  tfinds2  4836  tfinds3  4837  frsn  4941  ssrelrel  4969  relop  5016  iss  5182  poirr2  5251  xpcan  5298  xpcan2  5299  sossfld  5310  funopg  5478  funssres  5486  funun  5488  funcnvuni  5511  fv3  5737  fvmptt  5813  iinpreima  5853  suppss  5856  dff3  5875  dff4  5876  fnpr  5943  fnprOLD  5944  fvclss  5973  isomin  6050  isofrlem  6053  f1oweALT  6067  weniso  6068  oprabid  6098  f1o2ndf1  6447  poxp  6451  soxp  6452  fnse  6456  mpt2xopynvov0g  6458  reldmtpos  6480  rntpos  6485  onfununi  6596  smoiun  6616  tfrlem1  6629  tfr3  6653  frsucmptn  6689  tz7.49  6695  oaordi  6782  oawordeulem  6790  omeulem1  6818  oeordi  6823  oelimcl  6836  nnaordi  6854  nneob  6888  omsmolem  6889  erdisj  6945  qsss  6958  uniinqs  6977  th3qlem1  7003  map0g  7046  resixpfo  7093  ixpsnf1o  7095  xpdom3  7199  mapdom3  7272  phplem4  7282  php3  7286  unxpdomlem3  7308  ssfi  7322  findcard2  7341  findcard3  7343  frfi  7345  isfiniteg  7360  xpfi  7371  fiint  7376  finsschain  7406  dffi2  7421  marypha1lem  7431  marypha2  7437  supmo  7450  suplub2  7459  ordiso2  7477  ordtypelem7  7486  ordtypelem8  7487  brwdom2  7534  unxpwdom2  7549  ixpiunwdom  7552  elirrv  7558  suc11reg  7567  noinfep  7607  cantnfle  7619  cantnflem1  7638  cantnf  7642  trcl  7657  epfrs  7660  rankpwi  7742  rankunb  7769  rankuni2b  7772  rankxplim3  7798  cplem1  7806  karden  7812  carddom2  7857  fseqenlem2  7899  ac10ct  7908  acni2  7920  acndom  7925  infpwfien  7936  alephordi  7948  alephord  7949  iunfictbso  7988  aceq3lem  7994  dfac5  8002  dfac2  8004  dfac12lem3  8018  dfac12r  8019  cdainflem  8064  cdainf  8065  cfub  8122  cfeq0  8129  coflim  8134  cfslb2n  8141  cofsmo  8142  coftr  8146  infpssr  8181  fin23lem7  8189  fin23lem11  8190  fin23lem21  8212  isf32lem2  8227  isf34lem4  8250  isfin1-2  8258  isfin1-3  8259  fin1a2lem9  8281  fin1a2lem11  8283  fin1a2lem12  8284  fin1a2lem13  8285  domtriomlem  8315  axdc3lem2  8324  axcclem  8330  ac6c4  8354  zorn2lem4  8372  zorn2lem5  8373  zorn2lem7  8375  ttukeylem5  8386  ttukeyg  8390  brdom6disj  8403  fnrndomg  8406  iunfo  8407  iundom2g  8408  ficard  8433  konigthlem  8436  alephval2  8440  pwcfsdom  8451  fpwwe2lem9  8506  fpwwe2lem11  8508  fpwwe2lem12  8509  fpwwe2lem13  8510  pwfseqlem3  8528  gchpwdom  8542  winalim2  8564  gchina  8567  wunex2  8606  tskr1om2  8636  tskxpss  8640  inar1  8643  tskuni  8651  gruun  8674  grudomon  8685  grur1  8688  ltmpi  8774  ltexprlem2  8907  ltexprlem6  8911  reclem2pr  8918  reclem3pr  8919  reclem4pr  8920  suplem1pr  8922  mulgt0sr  8973  supsrlem  8979  axrrecex  9031  axpre-sup  9037  ltlen  9168  supmul1  9966  supmullem1  9967  supmullem2  9968  supmul  9969  infmrcl  9980  cju  9989  nnsub  10031  un0addcl  10246  un0mulcl  10247  nn0sub  10263  nn0n0n1ge2b  10274  peano5uzi  10351  negn0  10555  zsupss  10558  qbtwnre  10778  xrsupexmnf  10876  xrinfmexpnf  10877  xrsupsslem  10878  xrinfmsslem  10879  xrub  10883  supxrun  10887  xrinfm0  10908  ixxdisj  10924  icodisj  11015  difreicc  11021  elfznelfzo  11185  injresinj  11193  flval3  11215  modirr  11279  seqf1o  11357  expcl2lem  11386  expnegz  11407  expaddz  11417  expmulz  11419  facwordi  11573  faclbnd4lem4  11580  bccl  11606  hashnfinnn0  11636  hashgt12el  11675  hashgt12el2  11676  hashfun  11693  hashbclem  11694  hashbc  11695  hashfacen  11696  hashf1lem1  11697  hashf1  11699  brfi1uzind  11708  wrdind  11784  sqrlem1  12041  sqrlem6  12046  rexanre  12143  cau3lem  12151  2clim  12359  summo  12504  fsum2dlem  12547  fsumiun  12593  rpnnen2  12818  odd2np1lem  12900  bitsfzo  12940  sadcaddlem  12962  gcd0id  13016  algcvgblem  13061  prmdvdsexpr  13109  prmfac1  13111  qnumdencl  13124  hashdvds  13157  pcneg  13240  prmpwdvds  13265  prmreclem2  13278  4sqlem12  13317  vdwlem6  13347  vdwlem10  13351  vdwlem13  13354  0ram  13381  ram0  13383  ramz  13386  ramcl  13390  prmlem0  13421  firest  13653  imasaddfnlem  13746  imasvscafn  13755  mremre  13822  drsdirfi  14388  pospo  14423  lubun  14543  odupos  14555  acsfiindd  14596  psss  14639  odcau  15231  pgpfi  15232  sylow2blem3  15249  sylow3lem2  15255  lsmmod  15300  efgsfo  15364  frgpuptinv  15396  frgpnabllem1  15477  cyggeninv  15486  lt6abl  15497  cyggex2  15499  gsumval3  15507  gsum2d2  15541  dmdprdd  15553  dprd2da  15593  pgpfac1lem5  15630  pgpfac  15635  dvdsrtr  15750  dvdsrmul1  15751  lss1d  16032  lspsolvlem  16207  lspsnat  16210  lbsextlem2  16224  lbsextlem3  16225  domnmuln0  16351  abvn0b  16355  mvrf1  16482  opsrtoslem2  16538  xrsdsreclblem  16737  qsssubdrg  16751  prmirredlem  16766  cygznlem3  16843  obslbs  16950  unitg  17025  tgcl  17027  tgidm  17038  indistopon  17058  fctop  17061  cctop  17063  ppttop  17064  pptbas  17065  epttop  17066  opnnei  17177  neiptopnei  17189  tgrest  17216  restntr  17239  perfopn  17242  ordtrest2lem  17260  isreg2  17434  lmmo  17437  ordthauslem  17440  cmpsublem  17455  cmpsub  17456  cmpcld  17458  hauscmplem  17462  bwth  17466  iunconlem  17483  uncon  17485  2ndcrest  17510  2ndcctbss  17511  2ndcdisj  17512  dis2ndc  17516  txbas  17592  ptbasin  17602  ptbasfi  17606  txcls  17629  txbasval  17631  ptpjopn  17637  ptclsg  17640  dfac14lem  17642  xkoccn  17644  txcnp  17645  txindis  17659  txdis1cn  17660  tx1stc  17675  tx2ndc  17676  txkgen  17677  xkoco1cn  17682  xkoco2cn  17683  xkococn  17685  xkoinjcn  17712  txcon  17714  fbfinnfr  17866  opnfbas  17867  filtop  17880  isfild  17883  fbunfip  17894  filcon  17908  fbasrn  17909  filuni  17910  isufil2  17933  filssufilg  17936  ufileu  17944  filufint  17945  rnelfmlem  17977  rnelfm  17978  fmfnfmlem2  17980  fmfnfmlem4  17982  fmfnfm  17983  hausflimi  18005  hauspwpwf1  18012  flffbas  18020  flftg  18021  alexsublem  18068  alexsubALTlem1  18071  alexsubALTlem2  18072  alexsubALTlem3  18073  alexsubALTlem4  18074  alexsubALT  18075  ptcmplem3  18078  cldsubg  18133  divstgpopn  18142  tgptsmscld  18173  tsmsxplem1  18175  ustfilxp  18235  imasdsf1olem  18396  bldisj  18421  xbln0  18437  prdsxmslem2  18552  xrsblre  18835  icccmplem2  18847  reconn  18852  opnreen  18855  xrge0tsms  18858  metdsre  18876  iccpnfcnv  18962  cnheiborlem  18972  phtpc01  19014  pi1blem  19057  tchcph  19187  cfilfcls  19220  iscau4  19225  bcthlem5  19274  bcth3  19277  hlhil  19337  ovolctb  19379  ovoliunlem2  19392  ovoliunnul  19396  ovolicc2  19411  volfiniun  19434  iundisj  19435  dyadmax  19483  dyadmbllem  19484  vitalilem2  19494  ismbfd  19525  mbfimaopnlem  19540  itg11  19576  i1faddlem  19578  mbfi1fseqlem4  19603  bddmulibl  19723  limciun  19774  perfdvf  19783  rolle  19867  dvivthlem1  19885  dvne0  19888  lhop1  19891  lhop2  19892  itgsubst  19926  pf1ind  19968  dvdsq1p  20076  fta1g  20083  dgrco  20186  plydivex  20207  fta1  20218  ulmcaulem  20303  abelthlem2  20341  pilem2  20361  cxpmul2z  20575  cxpcn3lem  20624  xrlimcnp  20800  jensen  20820  wilthlem2  20845  wilthlem3  20846  muval2  20910  sqf11  20915  ppiublem1  20979  fsumvma  20990  lgsdir2lem2  21101  lgsdir2lem5  21104  dchrisum0fno1  21198  pntlem3  21296  pntleml  21298  ostthlem1  21314  ostth2lem2  21321  usgra2edg  21395  usgrares1  21417  nbgraf1olem5  21448  cusgrarn  21461  nbcusgra  21465  uvtxnbgra  21495  3v3e3cycl2  21644  vdusgra0nedg  21672  usgravd0nedg  21676  gxnn0neg  21844  gxnn0suc  21845  lnon0  22292  shmodsi  22884  shlub  22909  spanunsni  23074  h1datomi  23076  stm1ri  23740  stadd3i  23744  mdsl1i  23817  cvmdi  23820  superpos  23850  chjatom  23853  chirredi  23890  atcvat4i  23893  sumdmdii  23911  sumdmdlem  23914  cdj3lem2a  23932  cdj3lem3a  23935  cdj3i  23937  disji2f  24012  disjif2  24016  iundisjf  24022  rnmpt2ss  24079  iundisjfi  24145  xrge0tsmsd  24216  cnre2csqima  24302  xrge0iifcnv  24312  lmxrge0  24330  measdivcstOLD  24571  dya2iocuni  24626  derangenlem  24850  erdszelem9  24878  pconcon  24911  iccllyscon  24930  cvmsval  24946  cvmscld  24953  cvmsss2  24954  cvmopnlem  24958  cvmfolem  24959  cvmliftmolem2  24962  cvmlift2lem10  24992  cvmlift2lem12  24994  cvmlift3lem5  25003  cvmlift3lem8  25006  rtrclreclem.trans  25139  dfrtrcl2  25141  untsucf  25152  3orel1  25157  3orel2  25158  3orel3  25159  nepss  25168  mulge0b  25184  prodmo  25255  fprod2dlem  25297  dfon2lem5  25407  dfon2lem6  25408  dfon2lem7  25409  dfon2lem8  25410  rdgprc  25415  wfi  25475  wfis2fg  25479  trpredtr  25501  dftrpred3g  25504  trpredrec  25509  frmin  25510  frind  25511  frins2fg  25515  wfrlem14  25544  wfrlem15  25545  wsuclem  25569  frrlem5e  25583  nodenselem4  25632  nodenselem8  25636  nocvxmin  25639  nofulllem5  25654  funpartfun  25781  altopth1  25803  altopth2  25804  colinearalg  25842  axcontlem2  25897  axcontlem8  25903  colineardim1  25988  lineext  26003  btwnconn1lem14  26027  brsegle  26035  hilbert1.2  26082  bpolycl  26091  arg-ax  26159  ordtoplem  26178  onsuct0  26184  supaddc  26229  supadd  26230  mblfinlem  26235  mblfinlem3  26237  ovoliunnfl  26239  itg2addnclem  26247  itg2addnclem2  26248  areacirc  26289  trer  26311  elicc3  26312  finminlem  26313  fneint  26349  fnessref  26365  refssfne  26366  locfincmp  26376  comppfsc  26379  neibastop1  26380  neibastop2lem  26381  neibastop2  26382  fnemeet2  26388  fnejoin2  26390  tailfb  26398  unirep  26406  filbcmb  26434  fzadd2  26437  sdclem1  26439  fdc  26441  nninfnub  26447  isbnd2  26484  ssbnd  26489  prdsbnd2  26496  cntotbnd  26497  heibor1lem  26510  heiborlem1  26512  heiborlem4  26515  heiborlem6  26517  0idl  26627  intidl  26631  unichnidl  26633  keridl  26634  prnc  26669  ceqsex3OLD  26701  prtlem17  26717  prter2  26722  eldioph2b  26813  eldiophss  26825  diophren  26866  ctbnfien  26871  rencldnfilem  26873  pellexlem3  26886  pellexlem5  26888  pellex  26890  pell14qrexpcl  26922  pellfundre  26936  pellfundge  26937  pellfundlb  26939  pellfundglb  26940  jm2.19lem4  27055  fnwe2lem2  27118  pwssplit4  27160  dsmmacl  27176  lindfrn  27260  lmiclbs  27276  lmisfree  27281  hbtlem5  27301  f1omvdco2  27360  symggen  27380  hirstL-ax3  27828  2reurex  27927  eqneqall  28041  elnelall  28042  otiunsndisj  28057  otiunsndisjX  28058  0mnnnnn0  28081  elfzmlbp  28092  subsubelfzo0  28119  swrd0  28156  swrd0swrd  28164  swrdccatin1  28172  swrdccatin2  28177  swrdccat3  28182  swrdccat3blem  28185  cshwidx  28209  cshwidxmod  28210  2cshw1lem1  28215  cshw1  28239  cshwssizelem3  28246  usgra2pthspth  28259  3cyclfrgrarn1  28340  frgranbnb  28348  frgrancvvdeqlem3  28359  frgrancvvdeqlem4  28360  frgrancvvdeqlemC  28366  frgrawopreglem3  28373  frgrawopreglem4  28374  frgrawopreglem5  28375  frgrawopreg2  28378  2spotiundisj  28389  2spotmdisj  28395  onfrALT  28573  a9e2ndeq  28584  snssiALT  28878  bnj849  29234  bnj1118  29291  lubunNEW  29709  lsatn0  29735  lsatcmp  29739  lssat  29752  lfl1  29806  lshpsmreu  29845  lkrin  29900  glbconxN  30113  cvrat4  30178  paddasslem17  30571  pmodlem2  30582  dalawlem14  30619  pclclN  30626  pclfinN  30635  pclfinclN  30685  poml4N  30688  osumcllem8N  30698  pexmidlem5N  30709  cdleme32a  31176  cdlemg33b0  31436  tendoeq2  31509  diaelrnN  31781  dihmeetlem1N  32026  dihglblem5apreN  32027  dihglblem2N  32030  dochvalr  32093  dochkrshp  32122  lcfl6  32236  lcfrvalsnN  32277  mapdordlem2  32373  mapdh8b  32516  mapdh9a  32526  hdmap14lem13  32619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator