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  2249  2euex  2330  necon3bd  2608  necon2ad  2619  necon1ad  2638  pm2.61dne  2648  spcimgft  2991  rspc  3010  rspcimdv  3017  euind  3085  reuind  3101  sbciegft  3155  rspsbc  3203  pwpw0  3910  sssn  3921  eqsn  3924  prel12  3939  prnebg  3943  pwsnALT  3974  intss1  4029  intmin  4034  uniintsn  4051  iinss  4106  disji2  4163  disjiun  4166  disjxiun  4173  disjss3  4175  trel3  4274  trin  4276  trintss  4282  copsexg  4406  po3nr  4481  fri  4508  wefrc  4540  wereu2  4543  onfr  4584  ord0eln0  4599  onmindif  4634  eusvnfb  4682  reusv3  4694  ssorduni  4729  onmindif2  4755  limuni3  4795  tfis2f  4798  tfinds  4802  tfinds2  4806  tfinds3  4807  frsn  4911  ssrelrel  4939  relop  4986  iss  5152  poirr2  5221  xpcan  5268  xpcan2  5269  sossfld  5280  funopg  5448  funssres  5456  funun  5458  funcnvuni  5481  fv3  5707  fvmptt  5783  iinpreima  5823  suppss  5826  dff3  5845  dff4  5846  fnpr  5913  fnprOLD  5914  fvclss  5943  isomin  6020  isofrlem  6023  f1oweALT  6037  weniso  6038  oprabid  6068  f1o2ndf1  6417  poxp  6421  soxp  6422  fnse  6426  mpt2xopynvov0g  6428  reldmtpos  6450  rntpos  6455  onfununi  6566  smoiun  6586  tfrlem1  6599  tfr3  6623  frsucmptn  6659  tz7.49  6665  oaordi  6752  oawordeulem  6760  omeulem1  6788  oeordi  6793  oelimcl  6806  nnaordi  6824  nneob  6858  omsmolem  6859  erdisj  6915  qsss  6928  uniinqs  6947  th3qlem1  6973  map0g  7016  resixpfo  7063  ixpsnf1o  7065  xpdom3  7169  mapdom3  7242  phplem4  7252  php3  7256  unxpdomlem3  7278  ssfi  7292  findcard2  7311  findcard3  7313  frfi  7315  isfiniteg  7330  xpfi  7341  fiint  7346  finsschain  7375  dffi2  7390  marypha1lem  7400  marypha2  7406  supmo  7417  suplub2  7426  ordiso2  7444  ordtypelem7  7453  ordtypelem8  7454  brwdom2  7501  unxpwdom2  7516  ixpiunwdom  7519  elirrv  7525  suc11reg  7534  noinfep  7574  cantnfle  7586  cantnflem1  7605  cantnf  7609  trcl  7624  epfrs  7627  rankpwi  7709  rankunb  7736  rankuni2b  7739  rankxplim3  7765  cplem1  7773  karden  7779  carddom2  7824  fseqenlem2  7866  ac10ct  7875  acni2  7887  acndom  7892  infpwfien  7903  alephordi  7915  alephord  7916  iunfictbso  7955  aceq3lem  7961  dfac5  7969  dfac2  7971  dfac12lem3  7985  dfac12r  7986  cdainflem  8031  cdainf  8032  cfub  8089  cfeq0  8096  coflim  8101  cfslb2n  8108  cofsmo  8109  coftr  8113  infpssr  8148  fin23lem7  8156  fin23lem11  8157  fin23lem21  8179  isf32lem2  8194  isf34lem4  8217  isfin1-2  8225  isfin1-3  8226  fin1a2lem9  8248  fin1a2lem11  8250  fin1a2lem12  8251  fin1a2lem13  8252  domtriomlem  8282  axdc3lem2  8291  axcclem  8297  ac6c4  8321  zorn2lem4  8339  zorn2lem5  8340  zorn2lem7  8342  ttukeylem5  8353  ttukeyg  8357  brdom6disj  8370  fnrndomg  8373  iunfo  8374  iundom2g  8375  ficard  8400  konigthlem  8403  alephval2  8407  pwcfsdom  8418  fpwwe2lem9  8473  fpwwe2lem11  8475  fpwwe2lem12  8476  fpwwe2lem13  8477  pwfseqlem3  8495  gchpwdom  8509  winalim2  8531  gchina  8534  wunex2  8573  tskr1om2  8603  tskxpss  8607  inar1  8610  tskuni  8618  gruun  8641  grudomon  8652  grur1  8655  ltmpi  8741  ltexprlem2  8874  ltexprlem6  8878  reclem2pr  8885  reclem3pr  8886  reclem4pr  8887  suplem1pr  8889  mulgt0sr  8940  supsrlem  8946  axrrecex  8998  axpre-sup  9004  ltlen  9135  supmul1  9933  supmullem1  9934  supmullem2  9935  supmul  9936  infmrcl  9947  cju  9956  nnsub  9998  un0addcl  10213  un0mulcl  10214  nn0sub  10230  nn0n0n1ge2b  10241  peano5uzi  10318  negn0  10522  zsupss  10525  qbtwnre  10745  xrsupexmnf  10843  xrinfmexpnf  10844  xrsupsslem  10845  xrinfmsslem  10846  xrub  10850  supxrun  10854  xrinfm0  10875  ixxdisj  10891  icodisj  10982  difreicc  10988  elfznelfzo  11151  injresinj  11159  flval3  11181  modirr  11245  seqf1o  11323  expcl2lem  11352  expnegz  11373  expaddz  11383  expmulz  11385  facwordi  11539  faclbnd4lem4  11546  bccl  11572  hashnfinnn0  11602  hashgt12el  11641  hashgt12el2  11642  hashfun  11659  hashbclem  11660  hashbc  11661  hashfacen  11662  hashf1lem1  11663  hashf1  11665  brfi1uzind  11674  wrdind  11750  sqrlem1  12007  sqrlem6  12012  rexanre  12109  cau3lem  12117  2clim  12325  summo  12470  fsum2dlem  12513  fsumiun  12559  rpnnen2  12784  odd2np1lem  12866  bitsfzo  12906  sadcaddlem  12928  gcd0id  12982  algcvgblem  13027  prmdvdsexpr  13075  prmfac1  13077  qnumdencl  13090  hashdvds  13123  pcneg  13206  prmpwdvds  13231  prmreclem2  13244  4sqlem12  13283  vdwlem6  13313  vdwlem10  13317  vdwlem13  13320  0ram  13347  ram0  13349  ramz  13352  ramcl  13356  prmlem0  13387  firest  13619  imasaddfnlem  13712  imasvscafn  13721  mremre  13788  drsdirfi  14354  pospo  14389  lubun  14509  odupos  14521  acsfiindd  14562  psss  14605  odcau  15197  pgpfi  15198  sylow2blem3  15215  sylow3lem2  15221  lsmmod  15266  efgsfo  15330  frgpuptinv  15362  frgpnabllem1  15443  cyggeninv  15452  lt6abl  15463  cyggex2  15465  gsumval3  15473  gsum2d2  15507  dmdprdd  15519  dprd2da  15559  pgpfac1lem5  15596  pgpfac  15601  dvdsrtr  15716  dvdsrmul1  15717  lss1d  15998  lspsolvlem  16173  lspsnat  16176  lbsextlem2  16190  lbsextlem3  16191  domnmuln0  16317  abvn0b  16321  mvrf1  16448  opsrtoslem2  16504  xrsdsreclblem  16703  qsssubdrg  16717  prmirredlem  16732  cygznlem3  16809  obslbs  16916  unitg  16991  tgcl  16993  tgidm  17004  indistopon  17024  fctop  17027  cctop  17029  ppttop  17030  pptbas  17031  epttop  17032  opnnei  17143  neiptopnei  17155  tgrest  17181  restntr  17204  perfopn  17207  ordtrest2lem  17225  isreg2  17399  lmmo  17402  ordthauslem  17405  cmpsublem  17420  cmpsub  17421  cmpcld  17423  hauscmplem  17427  iunconlem  17447  uncon  17449  2ndcrest  17474  2ndcctbss  17475  2ndcdisj  17476  dis2ndc  17480  txbas  17556  ptbasin  17566  ptbasfi  17570  txcls  17593  txbasval  17595  ptpjopn  17601  ptclsg  17604  dfac14lem  17606  xkoccn  17608  txcnp  17609  txindis  17623  txdis1cn  17624  tx1stc  17639  tx2ndc  17640  txkgen  17641  xkoco1cn  17646  xkoco2cn  17647  xkococn  17649  xkoinjcn  17676  txcon  17678  fbfinnfr  17830  opnfbas  17831  filtop  17844  isfild  17847  fbunfip  17858  filcon  17872  fbasrn  17873  filuni  17874  isufil2  17897  filssufilg  17900  ufileu  17908  filufint  17909  rnelfmlem  17941  rnelfm  17942  fmfnfmlem2  17944  fmfnfmlem4  17946  fmfnfm  17947  hausflimi  17969  hauspwpwf1  17976  flffbas  17984  flftg  17985  alexsublem  18032  alexsubALTlem1  18035  alexsubALTlem2  18036  alexsubALTlem3  18037  alexsubALTlem4  18038  alexsubALT  18039  ptcmplem3  18042  cldsubg  18097  divstgpopn  18106  tgptsmscld  18137  tsmsxplem1  18139  ustfilxp  18199  imasdsf1olem  18360  bldisj  18385  xbln0  18401  prdsxmslem2  18516  xrsblre  18799  icccmplem2  18811  reconn  18816  opnreen  18819  xrge0tsms  18822  metdsre  18840  iccpnfcnv  18926  cnheiborlem  18936  phtpc01  18978  pi1blem  19021  tchcph  19151  cfilfcls  19184  iscau4  19189  bcthlem5  19238  bcth3  19241  hlhil  19301  ovolctb  19343  ovoliunlem2  19356  ovoliunnul  19360  ovolicc2  19375  volfiniun  19398  iundisj  19399  dyadmax  19447  dyadmbllem  19448  vitalilem2  19458  ismbfd  19489  mbfimaopnlem  19504  itg11  19540  i1faddlem  19542  mbfi1fseqlem4  19567  bddmulibl  19687  limciun  19738  perfdvf  19747  rolle  19831  dvivthlem1  19849  dvne0  19852  lhop1  19855  lhop2  19856  itgsubst  19890  pf1ind  19932  dvdsq1p  20040  fta1g  20047  dgrco  20150  plydivex  20171  fta1  20182  ulmcaulem  20267  abelthlem2  20305  pilem2  20325  cxpmul2z  20539  cxpcn3lem  20588  xrlimcnp  20764  jensen  20784  wilthlem2  20809  wilthlem3  20810  muval2  20874  sqf11  20879  ppiublem1  20943  fsumvma  20954  lgsdir2lem2  21065  lgsdir2lem5  21068  dchrisum0fno1  21162  pntlem3  21260  pntleml  21262  ostthlem1  21278  ostth2lem2  21285  usgra2edg  21359  usgrares1  21381  nbgraf1olem5  21412  cusgrarn  21425  nbcusgra  21429  uvtxnbgra  21459  3v3e3cycl2  21608  vdusgra0nedg  21636  usgravd0nedg  21640  gxnn0neg  21808  gxnn0suc  21809  lnon0  22256  shmodsi  22848  shlub  22873  spanunsni  23038  h1datomi  23040  stm1ri  23704  stadd3i  23708  mdsl1i  23781  cvmdi  23784  superpos  23814  chjatom  23817  chirredi  23854  atcvat4i  23857  sumdmdii  23875  sumdmdlem  23878  cdj3lem2a  23896  cdj3lem3a  23899  cdj3i  23901  disji2f  23976  disjif2  23980  iundisjf  23986  rnmpt2ss  24043  iundisjfi  24109  xrge0tsmsd  24180  cnre2csqima  24266  xrge0iifcnv  24276  lmxrge0  24294  measdivcstOLD  24535  dya2iocuni  24590  derangenlem  24814  erdszelem9  24842  pconcon  24875  iccllyscon  24894  cvmsval  24910  cvmscld  24917  cvmsss2  24918  cvmopnlem  24922  cvmfolem  24923  cvmliftmolem2  24926  cvmlift2lem10  24956  cvmlift2lem12  24958  cvmlift3lem5  24967  cvmlift3lem8  24970  rtrclreclem.trans  25103  dfrtrcl2  25105  untsucf  25116  3orel1  25121  3orel2  25122  3orel3  25123  nepss  25132  mulge0b  25148  prodmo  25219  fprod2dlem  25261  dfon2lem5  25361  dfon2lem6  25362  dfon2lem7  25363  dfon2lem8  25364  rdgprc  25369  wfi  25425  wfis2fg  25429  trpredtr  25451  dftrpred3g  25454  trpredrec  25459  frmin  25460  frind  25461  frins2fg  25465  wfrlem14  25487  wfrlem15  25488  frrlem5e  25507  nodenselem4  25556  nodenselem8  25560  nocvxmin  25563  nofulllem5  25578  funpartfun  25700  altopth1  25718  altopth2  25719  colinearalg  25757  axcontlem2  25812  axcontlem8  25818  colineardim1  25903  lineext  25918  btwnconn1lem14  25942  brsegle  25950  hilbert1.2  25997  bpolycl  26006  arg-ax  26074  ordtoplem  26093  onsuct0  26099  supaddc  26141  supadd  26142  mblfinlem  26147  mblfinlem3  26149  ovoliunnfl  26151  itg2addnclem  26159  itg2addnclem2  26160  areacirc  26191  trer  26213  elicc3  26214  finminlem  26215  fneint  26251  fnessref  26267  refssfne  26268  locfincmp  26278  comppfsc  26281  neibastop1  26282  neibastop2lem  26283  neibastop2  26284  fnemeet2  26290  fnejoin2  26292  tailfb  26300  unirep  26308  filbcmb  26336  fzadd2  26339  sdclem1  26341  fdc  26343  nninfnub  26349  isbnd2  26386  ssbnd  26391  prdsbnd2  26398  cntotbnd  26399  heibor1lem  26412  heiborlem1  26414  heiborlem4  26417  heiborlem6  26419  0idl  26529  intidl  26533  unichnidl  26535  keridl  26536  prnc  26571  ceqsex3OLD  26603  prtlem17  26619  prter2  26624  eldioph2b  26715  eldiophss  26727  diophren  26768  ctbnfien  26773  rencldnfilem  26775  pellexlem3  26788  pellexlem5  26790  pellex  26792  pell14qrexpcl  26824  pellfundre  26838  pellfundge  26839  pellfundlb  26841  pellfundglb  26842  jm2.19lem4  26957  fnwe2lem2  27020  pwssplit4  27063  dsmmacl  27079  lindfrn  27163  lmiclbs  27179  lmisfree  27184  hbtlem5  27204  f1omvdco2  27263  symggen  27283  hirstL-ax3  27731  2reurex  27830  eqneqall  27943  elnelall  27944  otiunsndisj  27958  otiunsndisjX  27959  0mnnnnn0  27975  elfzmlbp  27982  swrd0  28006  swrd0swrd  28013  swrdccatin1  28020  swrdccatin12b  28031  swrdccat3  28033  swrdccat3b  28035  usgra2pthspth  28039  3cyclfrgrarn1  28120  frgranbnb  28128  frgrancvvdeqlem3  28139  frgrancvvdeqlem4  28140  frgrancvvdeqlemC  28146  frgrawopreglem3  28153  frgrawopreglem4  28154  frgrawopreglem5  28155  frgrawopreg2  28158  2spotiundisj  28169  2spotmdisj  28175  onfrALT  28350  a9e2ndeq  28361  snssiALT  28653  bnj849  29006  bnj1118  29063  lubunNEW  29460  lsatn0  29486  lsatcmp  29490  lssat  29503  lfl1  29557  lshpsmreu  29596  lkrin  29651  glbconxN  29864  cvrat4  29929  paddasslem17  30322  pmodlem2  30333  dalawlem14  30370  pclclN  30377  pclfinN  30386  pclfinclN  30436  poml4N  30439  osumcllem8N  30449  pexmidlem5N  30460  cdleme32a  30927  cdlemg33b0  31187  tendoeq2  31260  diaelrnN  31532  dihmeetlem1N  31777  dihglblem5apreN  31778  dihglblem2N  31781  dochvalr  31844  dochkrshp  31873  lcfl6  31987  lcfrvalsnN  32028  mapdordlem2  32124  mapdh8b  32267  mapdh9a  32277  hdmap14lem13  32370
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