MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bi 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  1658  19.9htOLD  1799  19.9tOLD  1876  ax12olem5OLD  1981  ax11indn  2245  2euex  2326  necon3bd  2604  necon2ad  2615  necon1ad  2634  pm2.61dne  2644  spcimgft  2987  rspc  3006  rspcimdv  3013  euind  3081  reuind  3097  sbciegft  3151  rspsbc  3199  pwpw0  3906  sssn  3917  eqsn  3920  prel12  3935  prnebg  3939  pwsnALT  3970  intss1  4025  intmin  4030  uniintsn  4047  iinss  4102  disji2  4159  disjiun  4162  disjxiun  4169  disjss3  4171  trel3  4270  trin  4272  trintss  4278  copsexg  4402  po3nr  4477  fri  4504  wefrc  4536  wereu2  4539  onfr  4580  ord0eln0  4595  onmindif  4630  eusvnfb  4678  reusv3  4690  ssorduni  4725  onmindif2  4751  limuni3  4791  tfis2f  4794  tfinds  4798  tfinds2  4802  tfinds3  4803  frsn  4907  ssrelrel  4935  relop  4982  iss  5148  poirr2  5217  xpcan  5264  xpcan2  5265  sossfld  5276  funopg  5444  funssres  5452  funun  5454  funcnvuni  5477  fv3  5703  fvmptt  5779  iinpreima  5819  suppss  5822  dff3  5841  dff4  5842  fnpr  5909  fnprOLD  5910  fvclss  5939  isomin  6016  isofrlem  6019  f1oweALT  6033  weniso  6034  oprabid  6064  f1o2ndf1  6413  poxp  6417  soxp  6418  fnse  6422  mpt2xopynvov0g  6424  reldmtpos  6446  rntpos  6451  onfununi  6562  smoiun  6582  tfrlem1  6595  tfr3  6619  frsucmptn  6655  tz7.49  6661  oaordi  6748  oawordeulem  6756  omeulem1  6784  oeordi  6789  oelimcl  6802  nnaordi  6820  nneob  6854  omsmolem  6855  erdisj  6911  qsss  6924  uniinqs  6943  th3qlem1  6969  map0g  7012  resixpfo  7059  ixpsnf1o  7061  xpdom3  7165  mapdom3  7238  phplem4  7248  php3  7252  unxpdomlem3  7274  ssfi  7288  findcard2  7307  findcard3  7309  frfi  7311  isfiniteg  7326  xpfi  7337  fiint  7342  finsschain  7371  dffi2  7386  marypha1lem  7396  marypha2  7402  supmo  7413  suplub2  7422  ordiso2  7440  ordtypelem7  7449  ordtypelem8  7450  brwdom2  7497  unxpwdom2  7512  ixpiunwdom  7515  elirrv  7521  suc11reg  7530  noinfep  7570  cantnfle  7582  cantnflem1  7601  cantnf  7605  trcl  7620  epfrs  7623  rankpwi  7705  rankunb  7732  rankuni2b  7735  rankxplim3  7761  cplem1  7769  karden  7775  carddom2  7820  fseqenlem2  7862  ac10ct  7871  acni2  7883  acndom  7888  infpwfien  7899  alephordi  7911  alephord  7912  iunfictbso  7951  aceq3lem  7957  dfac5  7965  dfac2  7967  dfac12lem3  7981  dfac12r  7982  cdainflem  8027  cdainf  8028  cfub  8085  cfeq0  8092  coflim  8097  cfslb2n  8104  cofsmo  8105  coftr  8109  infpssr  8144  fin23lem7  8152  fin23lem11  8153  fin23lem21  8175  isf32lem2  8190  isf34lem4  8213  isfin1-2  8221  isfin1-3  8222  fin1a2lem9  8244  fin1a2lem11  8246  fin1a2lem12  8247  fin1a2lem13  8248  domtriomlem  8278  axdc3lem2  8287  axcclem  8293  ac6c4  8317  zorn2lem4  8335  zorn2lem5  8336  zorn2lem7  8338  ttukeylem5  8349  ttukeyg  8353  brdom6disj  8366  fnrndomg  8369  iunfo  8370  iundom2g  8371  ficard  8396  konigthlem  8399  alephval2  8403  pwcfsdom  8414  fpwwe2lem9  8469  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  pwfseqlem3  8491  gchpwdom  8505  winalim2  8527  gchina  8530  wunex2  8569  tskr1om2  8599  tskxpss  8603  inar1  8606  tskuni  8614  gruun  8637  grudomon  8648  grur1  8651  ltmpi  8737  ltexprlem2  8870  ltexprlem6  8874  reclem2pr  8881  reclem3pr  8882  reclem4pr  8883  suplem1pr  8885  mulgt0sr  8936  supsrlem  8942  axrrecex  8994  axpre-sup  9000  ltlen  9131  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  infmrcl  9943  cju  9952  nnsub  9994  un0addcl  10209  un0mulcl  10210  nn0sub  10226  nn0n0n1ge2b  10237  peano5uzi  10314  negn0  10518  zsupss  10521  qbtwnre  10741  xrsupexmnf  10839  xrinfmexpnf  10840  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrun  10850  xrinfm0  10871  ixxdisj  10887  icodisj  10978  difreicc  10984  elfznelfzo  11147  injresinj  11155  flval3  11177  modirr  11241  seqf1o  11319  expcl2lem  11348  expnegz  11369  expaddz  11379  expmulz  11381  facwordi  11535  faclbnd4lem4  11542  bccl  11568  hashnfinnn0  11598  hashgt12el  11637  hashgt12el2  11638  hashfun  11655  hashbclem  11656  hashbc  11657  hashfacen  11658  hashf1lem1  11659  hashf1  11661  brfi1uzind  11670  wrdind  11746  sqrlem1  12003  sqrlem6  12008  rexanre  12105  cau3lem  12113  2clim  12321  summo  12466  fsum2dlem  12509  fsumiun  12555  rpnnen2  12780  odd2np1lem  12862  bitsfzo  12902  sadcaddlem  12924  gcd0id  12978  algcvgblem  13023  prmdvdsexpr  13071  prmfac1  13073  qnumdencl  13086  hashdvds  13119  pcneg  13202  prmpwdvds  13227  prmreclem2  13240  4sqlem12  13279  vdwlem6  13309  vdwlem10  13313  vdwlem13  13316  0ram  13343  ram0  13345  ramz  13348  ramcl  13352  prmlem0  13383  firest  13615  imasaddfnlem  13708  imasvscafn  13717  mremre  13784  drsdirfi  14350  pospo  14385  lubun  14505  odupos  14517  acsfiindd  14558  psss  14601  odcau  15193  pgpfi  15194  sylow2blem3  15211  sylow3lem2  15217  lsmmod  15262  efgsfo  15326  frgpuptinv  15358  frgpnabllem1  15439  cyggeninv  15448  lt6abl  15459  cyggex2  15461  gsumval3  15469  gsum2d2  15503  dmdprdd  15515  dprd2da  15555  pgpfac1lem5  15592  pgpfac  15597  dvdsrtr  15712  dvdsrmul1  15713  lss1d  15994  lspsolvlem  16169  lspsnat  16172  lbsextlem2  16186  lbsextlem3  16187  domnmuln0  16313  abvn0b  16317  mvrf1  16444  opsrtoslem2  16500  xrsdsreclblem  16699  qsssubdrg  16713  prmirredlem  16728  cygznlem3  16805  obslbs  16912  unitg  16987  tgcl  16989  tgidm  17000  indistopon  17020  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  epttop  17028  opnnei  17139  neiptopnei  17151  tgrest  17177  restntr  17200  perfopn  17203  ordtrest2lem  17221  isreg2  17395  lmmo  17398  ordthauslem  17401  cmpsublem  17416  cmpsub  17417  cmpcld  17419  hauscmplem  17423  iunconlem  17443  uncon  17445  2ndcrest  17470  2ndcctbss  17471  2ndcdisj  17472  dis2ndc  17476  txbas  17552  ptbasin  17562  ptbasfi  17566  txcls  17589  txbasval  17591  ptpjopn  17597  ptclsg  17600  dfac14lem  17602  xkoccn  17604  txcnp  17605  txindis  17619  txdis1cn  17620  tx1stc  17635  tx2ndc  17636  txkgen  17637  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  txcon  17674  fbfinnfr  17826  opnfbas  17827  filtop  17840  isfild  17843  fbunfip  17854  filcon  17868  fbasrn  17869  filuni  17870  isufil2  17893  filssufilg  17896  ufileu  17904  filufint  17905  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  hausflimi  17965  hauspwpwf1  17972  flffbas  17980  flftg  17981  alexsublem  18028  alexsubALTlem1  18031  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem3  18038  cldsubg  18093  divstgpopn  18102  tgptsmscld  18133  tsmsxplem1  18135  ustfilxp  18195  imasdsf1olem  18356  bldisj  18381  xbln0  18397  prdsxmslem2  18512  xrsblre  18795  icccmplem2  18807  reconn  18812  opnreen  18815  xrge0tsms  18818  metdsre  18836  iccpnfcnv  18922  cnheiborlem  18932  phtpc01  18974  pi1blem  19017  tchcph  19147  cfilfcls  19180  iscau4  19185  bcthlem5  19234  bcth3  19237  hlhil  19297  ovolctb  19339  ovoliunlem2  19352  ovoliunnul  19356  ovolicc2  19371  volfiniun  19394  iundisj  19395  dyadmax  19443  dyadmbllem  19444  vitalilem2  19454  ismbfd  19485  mbfimaopnlem  19500  itg11  19536  i1faddlem  19538  mbfi1fseqlem4  19563  bddmulibl  19683  limciun  19734  perfdvf  19743  rolle  19827  dvivthlem1  19845  dvne0  19848  lhop1  19851  lhop2  19852  itgsubst  19886  pf1ind  19928  dvdsq1p  20036  fta1g  20043  dgrco  20146  plydivex  20167  fta1  20178  ulmcaulem  20263  abelthlem2  20301  pilem2  20321  cxpmul2z  20535  cxpcn3lem  20584  xrlimcnp  20760  jensen  20780  wilthlem2  20805  wilthlem3  20806  muval2  20870  sqf11  20875  ppiublem1  20939  fsumvma  20950  lgsdir2lem2  21061  lgsdir2lem5  21064  dchrisum0fno1  21158  pntlem3  21256  pntleml  21258  ostthlem1  21274  ostth2lem2  21281  usgra2edg  21355  usgrares1  21377  nbgraf1olem5  21408  cusgrarn  21421  nbcusgra  21425  uvtxnbgra  21455  3v3e3cycl2  21604  vdusgra0nedg  21632  usgravd0nedg  21636  gxnn0neg  21804  gxnn0suc  21805  lnon0  22252  shmodsi  22844  shlub  22869  spanunsni  23034  h1datomi  23036  stm1ri  23700  stadd3i  23704  mdsl1i  23777  cvmdi  23780  superpos  23810  chjatom  23813  chirredi  23850  atcvat4i  23853  sumdmdii  23871  sumdmdlem  23874  cdj3lem2a  23892  cdj3lem3a  23895  cdj3i  23897  disji2f  23972  disjif2  23976  iundisjf  23982  rnmpt2ss  24039  iundisjfi  24105  xrge0tsmsd  24176  cnre2csqima  24262  xrge0iifcnv  24272  lmxrge0  24290  measdivcstOLD  24531  dya2iocuni  24586  derangenlem  24810  erdszelem9  24838  pconcon  24871  iccllyscon  24890  cvmsval  24906  cvmscld  24913  cvmsss2  24914  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem2  24922  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift3lem5  24963  cvmlift3lem8  24966  rtrclreclem.trans  25099  dfrtrcl2  25101  untsucf  25112  3orel1  25117  3orel2  25118  3orel3  25119  nepss  25128  mulge0b  25144  prodmo  25215  fprod2dlem  25257  dfon2lem5  25357  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  rdgprc  25365  wfi  25421  wfis2fg  25425  trpredtr  25447  dftrpred3g  25450  trpredrec  25455  frmin  25456  frind  25457  frins2fg  25461  wfrlem14  25483  wfrlem15  25484  frrlem5e  25503  nodenselem4  25552  nodenselem8  25556  nocvxmin  25559  nofulllem5  25574  funpartfun  25696  altopth1  25714  altopth2  25715  colinearalg  25753  axcontlem2  25808  axcontlem8  25814  colineardim1  25899  lineext  25914  btwnconn1lem14  25938  brsegle  25946  hilbert1.2  25993  bpolycl  26002  arg-ax  26070  ordtoplem  26089  onsuct0  26095  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem3  26145  ovoliunnfl  26147  itg2addnclem  26155  itg2addnclem2  26156  areacirc  26187  trer  26209  elicc3  26210  finminlem  26211  fneint  26247  fnessref  26263  refssfne  26264  locfincmp  26274  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  fnemeet2  26286  fnejoin2  26288  tailfb  26296  unirep  26304  filbcmb  26332  fzadd2  26335  sdclem1  26337  fdc  26339  nninfnub  26345  isbnd2  26382  ssbnd  26387  prdsbnd2  26394  cntotbnd  26395  heibor1lem  26408  heiborlem1  26410  heiborlem4  26413  heiborlem6  26415  0idl  26525  intidl  26529  unichnidl  26531  keridl  26532  prnc  26567  ceqsex3OLD  26599  prtlem17  26615  prter2  26620  eldioph2b  26711  eldiophss  26723  diophren  26764  ctbnfien  26769  rencldnfilem  26771  pellexlem3  26784  pellexlem5  26786  pellex  26788  pell14qrexpcl  26820  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  jm2.19lem4  26953  fnwe2lem2  27016  pwssplit4  27059  dsmmacl  27075  lindfrn  27159  lmiclbs  27175  lmisfree  27180  hbtlem5  27200  f1omvdco2  27259  symggen  27279  hirstL-ax3  27727  2reurex  27826  eqneqall  27939  elnelall  27940  otiunsndisj  27954  otiunsndisjX  27955  0mnnnnn0  27971  elfzmlbp  27978  swrd0  28002  swrd0swrd  28009  swrdccatin1  28016  swrdccatin12b  28027  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  3cyclfrgrarn1  28116  frgranbnb  28124  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrancvvdeqlemC  28142  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreglem5  28151  frgrawopreg2  28154  2spotiundisj  28165  2spotmdisj  28171  onfrALT  28346  a9e2ndeq  28357  snssiALT  28649  bnj849  29002  bnj1118  29059  lubunNEW  29456  lsatn0  29482  lsatcmp  29486  lssat  29499  lfl1  29553  lshpsmreu  29592  lkrin  29647  glbconxN  29860  cvrat4  29925  paddasslem17  30318  pmodlem2  30329  dalawlem14  30366  pclclN  30373  pclfinN  30382  pclfinclN  30432  poml4N  30435  osumcllem8N  30445  pexmidlem5N  30456  cdleme32a  30923  cdlemg33b0  31183  tendoeq2  31256  diaelrnN  31528  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem2N  31777  dochvalr  31840  dochkrshp  31869  lcfl6  31983  lcfrvalsnN  32024  mapdordlem2  32120  mapdh8b  32263  mapdh9a  32273  hdmap14lem13  32366
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