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

Theorem sylbid 206
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
sylbid.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
sylbid  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4d  259  ax11eq  2145  ax11el  2146  nlimsucg  4649  poltletr  5094  xp11  5127  xpcan  5128  xpcan2  5129  foconst  5478  fvmptdf  5627  suppss  5674  soisores  5840  isomin  5850  weniso  5868  ovmpt2df  5995  riotaxfrd  6352  eusvobj2  6353  smoiso  6395  tfrlem5  6412  tz7.48lem  6469  oevn0  6530  oaass  6575  omword1  6587  omlimcl  6592  odi  6593  oneo  6595  omeulem1  6596  oewordi  6605  oeworde  6607  oelimcl  6614  oaabs2  6659  omabs  6661  nnneo  6665  dom2lem  6917  fundmen  6950  onfin  7067  domfi  7100  dif1enOLD  7106  dif1en  7107  isfinite2  7131  unfilem1  7137  elfiun  7199  dffi3  7200  supisoex  7238  ordiso2  7246  ordtypelem7  7255  brwdom3  7312  unxpwdom2  7318  noinfepOLD  7377  cantnflem1  7407  cantnf  7411  r1sdom  7462  r1ord3g  7467  rankr1ai  7486  rankonidlem  7516  bndrank  7529  rankunb  7538  tcrank  7570  wdomfil  7704  wdomnumr  7707  alephordi  7717  alephdom  7724  dfac3  7764  dfac12lem3  7787  cfeq0  7898  cfsmolem  7912  sornom  7919  fin23lem28  7982  fin23lem30  7984  isf32lem2  7996  fin1a2lem9  8050  axcc2lem  8078  axdc3lem2  8093  axdc4lem  8097  ttukeylem5  8156  alephreg  8220  pwcfsdom  8221  fpwwe2lem13  8280  fpwwe2  8281  pwfseqlem3  8298  gchina  8337  inatsk  8416  intgru  8452  grur1  8458  grutsk1  8459  addcanpi  8539  mulcanpi  8540  addnidpi  8541  ltexnq  8615  ltbtwnnq  8618  genpss  8644  genpcd  8646  genpnmax  8647  addclprlem1  8656  mulclprlem  8659  distrlem1pr  8665  distrlem4pr  8666  distrlem5pr  8667  ltexprlem3  8678  ltexprlem6  8681  ltexpri  8683  reclem4pr  8690  axpre-sup  8807  lelttr  8928  ltletr  8929  letr  8930  le2add  9272  ltleadd  9273  lt2sub  9288  le2sub  9289  mulge0  9307  prodgt0  9617  squeeze0  9675  addltmul  9963  elnnz  10050  zextlt  10102  uzind2  10120  uzindOLD  10122  indstr  10303  qreccl  10352  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  xrlelttr  10503  xrltletr  10504  xrletr  10505  xrrebnd  10513  qbtwnre  10542  qbtwnxr  10543  qextlt  10546  qextle  10547  xltnegi  10559  xmulasslem  10621  xlemul1a  10624  iccid  10717  icoshft  10774  prunioo  10780  difreicc  10783  iccsplit  10784  fzm1  10878  modirr  11025  om2uzf1oi  11032  seqf1olem1  11101  sqlecan  11225  facdiv  11316  facwordi  11318  faclbnd  11319  bcpasc  11349  hashdom  11377  seqcoll  11417  sqrlem6  11749  resqrex  11752  absnid  11799  cau3lem  11854  sqreu  11860  rlim2lt  11987  rlim3  11988  o1lo1  12027  o1lo12  12028  rlimuni  12040  climuni  12042  lo1resb  12054  o1resb  12056  2clim  12062  o1rlimmul  12108  lo1le  12141  fsumss  12214  fsumabs  12275  cvgcmpce  12292  geomulcvg  12348  mertenslem2  12357  reeff1  12416  efieq1re  12495  dvdsmultr2  12580  dvdsleabs  12591  odd2np1lem  12602  odd2np1  12603  divalglem8  12615  sadcaddlem  12664  gcdneg  12721  gcddiv  12744  dvdssqim  12748  algcvga  12765  prmind2  12785  coprmdvds  12797  coprmdvds2  12798  qredeq  12801  euclemma  12803  nprmdvds1  12806  prmdvdsexpr  12811  prmfac1  12813  divgcdodd  12814  crt  12862  eulerthlem2  12866  fermltl  12868  coprimeprodsq2  12879  pythagtriplem2  12886  iserodd  12904  pcpremul  12912  pcdvdsb  12937  pc2dvds  12947  pc11  12948  pcfac  12963  prmpwdvds  12967  prmreclem4  12982  prmreclem5  12983  1arith  12990  4sqlem11  13018  vdwlem6  13049  vdwlem7  13050  vdwlem9  13052  vdwlem10  13053  vdwlem11  13054  ramub1lem2  13090  ramcl  13092  prmlem0  13123  firest  13353  imasaddfnlem  13446  imasvscafn  13455  erlecpbl  13468  xpsff1o  13486  setcmon  13935  setcepi  13936  setciso  13939  pltnle  14116  pltletr  14121  plelttr  14122  psref  14333  dirge  14375  imasmnd2  14425  imasgrp2  14626  ghmpreima  14720  gaorber  14778  mndodcongi  14874  sylow1lem1  14925  odcau  14931  sylow2alem1  14944  sylow2alem2  14945  lsmsubm  14980  lsmsubg  14981  lsmmod  15000  lsmdisj2  15007  efgtlen  15051  efgredlemc  15070  efgcpbllemb  15080  torsubg  15162  frgpnabllem1  15177  cyggexb  15201  gsumval3a  15205  dprdsubg  15275  dprddisj2  15290  dmdprdsplit2lem  15296  dmdprdsplit2  15297  ablfacrp  15317  ablfac1eulem  15323  pgpfac1lem3  15328  imasrng  15418  unitgrp  15465  lmhmima  15820  lsmcl  15852  lsmelval2  15854  lspsneleq  15884  lpiss  16018  xrsdsreclb  16434  gzrngunitlem  16452  znidomb  16531  frgpcyg  16543  tgtop  16727  neips  16866  neindisj  16870  restbas  16905  tgrest  16906  restcld  16919  restcldr  16921  ordtbas2  16937  ordtbas  16938  tgcn  16998  tgcnp  16999  subbascn  17000  cnconst2  17027  cnconst  17028  cnpresti  17032  cmpsublem  17142  tgcmp  17144  uncmp  17146  hauscmplem  17149  conndisj  17158  nconsubb  17165  1stcfb  17187  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  1stccnp  17204  llyrest  17227  nllyrest  17228  nllyidm  17231  cldllycmp  17237  1stckgen  17265  txcls  17315  txbasval  17317  txcnpi  17318  txcnp  17330  ptcnplem  17331  txdis1cn  17345  txlly  17346  txnlly  17347  pthaus  17348  tx1stc  17360  xkohaus  17363  xkococn  17370  basqtop  17418  qtopeu  17423  qtoprest  17424  qtopomap  17425  qtopcmap  17426  kqfvima  17437  kqsat  17438  kqcldsat  17440  fbfinnfr  17552  fgfil  17586  fgabs  17590  trfil2  17598  ufilmax  17618  isufil2  17619  ufprim  17620  ufileu  17630  filufint  17631  cfinufil  17639  elfm2  17659  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  ufldom  17673  flffbas  17706  flimfnfcls  17739  alexsublem  17754  alexsubALT  17761  symgtgp  17800  divstgpopn  17818  divstgplem  17819  tsmsxplem1  17851  bldisj  17971  xbln0  17981  blss  17988  blin2  17991  blcls  18068  prdsxmslem2  18091  xrsblre  18333  xrsmopn  18334  recld2  18336  reperflem  18339  reconnlem2  18348  cnmpt2pc  18442  cnheibor  18469  lebnumlem3  18477  nmhmcn  18617  cphsqrcl2  18638  iscau3  18720  iscau4  18721  iscmet3lem2  18734  lmcau  18754  cmetss  18756  bcth3  18769  minveclem3b  18808  ivthlem2  18828  ivthlem3  18829  ovolctb  18865  ovolscalem1  18888  ovolicc2lem3  18894  ovolicc2lem4  18895  dyaddisjlem  18966  dyadmbllem  18970  opnmbllem  18972  subopnmbl  18975  volivth  18978  mbfimaopn2  19028  i1faddlem  19064  i1fmullem  19065  itg10a  19081  itg1ge0a  19082  mbfi1fseqlem4  19089  mbfi1flimlem  19093  dveflem  19342  dvlip2  19358  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvcvx  19383  dvfsumrlim  19394  ftc1lem6  19404  itgsubst  19412  coe1mul3  19501  dvdsq1p  19562  coemullem  19647  coe1termlem  19655  dgrco  19672  coecj  19675  aaliou3lem7  19745  ulmcn  19792  reeff1o  19839  sincosq3sgn  19884  sincosq4sgn  19885  sineq0  19905  recosf1o  19913  efopn  20021  cxpge0  20046  cxpcn3lem  20103  cxpeq  20113  angpieqvd  20144  atantayl2  20250  rlimcnp  20276  xrlimcnp  20279  cxploglim  20288  ftalem2  20327  muval1  20387  ppiublem1  20457  chtub  20467  dchrmulcl  20504  dchrsum2  20523  bclbnd  20535  bposlem1  20539  bposlem5  20543  lgsdirnn0  20594  lgsqrlem2  20597  lgseisenlem2  20605  lgsquadlem1  20609  2sqblem  20632  chtppilimlem2  20639  dchrisumlem3  20656  dchrisum0lem1  20681  pntlem3  20774  ostth2lem2  20799  ostth3  20803  isabloda  20982  blocnilem  21398  ipasslem11  21434  h1de2ctlem  22150  spansneleq  22165  spansnss  22166  normcan  22171  spansncvi  22247  nmcexi  22622  elpjrn  22786  stadd3i  22844  cvcon3  22880  dmdbr5  22904  ssdmd2  22910  atom1d  22949  superpos  22950  cvexchlem  22964  atcv0eq  22975  atexch  22977  atcvat4i  22993  atdmd  22994  atmd2  22996  mdsymlem3  23001  mdsymlem5  23003  sumdmdlem  23014  cdjreui  23028  cnre2csqlem  23309  cnre2csqima  23310  erdszelem4  23740  erdszelem9  23745  sconpi1  23785  relexpsucl  24043  rtrclreclem.trans  24058  mulge0b  24101  dvdspw  24174  predpo  24255  uzsinds  24287  omsinds  24290  soseq  24325  sltres  24389  nodenselem3  24408  nodenselem4  24409  nodenselem5  24410  nodenselem8  24413  nofulllem5  24431  brbtwn2  24605  colinearalg  24610  axbtwnid  24639  axlowdimlem14  24655  axlowdimlem15  24656  axcontlem2  24665  cgrid2  24698  cgrextend  24703  btwnswapid2  24713  btwnexch3  24715  btwnexch  24720  ifscgr  24739  btwnxfr  24751  colineardim1  24756  colinearxfr  24770  lineext  24771  fscgr  24775  brsegle2  24804  seglecgr12im  24805  seglecgr12  24806  segletr  24809  segleantisym  24810  colinbtwnle  24813  broutsideof2  24817  outsideofeq  24825  outsidele  24827  lineunray  24842  lineelsb2  24843  elhf2  24877  ordtopcon  24950  ordtopt0  24953  ovoliunnfl  25001  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  ftc1cnnc  25025  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  areacirclem5  25032  areacirc  25034  copsexgb  25069  repfuntw  25263  elioo1t3  25605  cmptdst  25671  islimrs3  25684  bwt2  25695  iintlem1  25713  dualded  25886  ismonb2  25915  icmpmon  25919  idmon  25920  isepib2  25925  lineval5a  26191  lineval6a  26192  segline  26244  nn0prpwlem  26341  nn0prpw  26342  cldbnd  26347  fgmin  26422  tailfb  26429  indexdom  26516  fzmul  26546  fzadd2  26547  sdclem2  26555  sdclem1  26556  fdc  26558  incsequz  26561  sstotbnd2  26601  equivbnd  26617  prdstotbnd  26621  grpokerinj  26678  keridl  26760  smprngopr  26780  ispridlc  26798  dmncan2  26805  diophin  26955  diophun  26956  fphpdo  27003  pellexlem1  27017  pell1234qrne0  27041  pell14qrgt0  27047  pell1234qrdich  27049  pell1qrge1  27058  elpell1qr2  27060  pell1qrgap  27062  pellfundex  27074  rmxypairf1o  27099  jm2.26a  27196  setindtr  27220  rpnnen3  27228  dnnumch3  27247  fnwe2lem2  27251  pwssplit4  27294  lindfrn  27394  f1lindf  27395  hbtlem5  27435  pmtrfrn  27503  symggen  27514  psgnunilem2  27521  elfznelfzo  28213  injresinjlem  28214  hashtpg  28217  hashgt12el  28218  hashgt12el2  28219  usgra0v  28251  usgraedgrn  28259  usgra1v  28260  nbusgra  28277  nbgraisvtx  28280  nb3graprlem1  28287  uvtxnbgra  28306  cusgrauvtx  28309  trliswlk  28338  trlonprop  28341  pthdepisspth  28360  redwlk  28364  cyclnspth  28376  fargshiftf1  28382  usgrcyclnl1  28386  usgrcyclnl2  28387  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  3vfriswmgra  28429  1to2vfriswmgra  28430  lshpdisj  29799  lsat0cv  29845  lcvexchlem4  29849  lcvexchlem5  29850  lsatcv0eq  29859  lfl1dim  29933  lfl1dim2N  29934  lkrss2N  29981  lkreqN  29982  cmtbr3N  30066  omlfh3N  30071  cvrnbtwn  30083  cvrcon3b  30089  atnle  30129  cvlatexch1  30148  cvlsupr2  30155  hlrelat2  30214  cvrexchlem  30230  cvrat  30233  atcvr0eq  30237  atcvrj0  30239  atltcvr  30246  cvrat4  30254  lvolex3N  30349  islpln2a  30359  lplnriaN  30361  llncvrlpln2  30368  islvol2aN  30403  lplncvrlvol2  30426  dalem-cly  30482  dalem44  30527  snatpsubN  30561  pointpsubN  30562  lncvrelatN  30592  cdlemblem  30604  paddasslem16  30646  paddidm  30652  pmodlem2  30658  pmapjoin  30663  llnexchb2  30680  llnexch2N  30681  pclfinclN  30761  linepsubclN  30762  lhpj1  30833  lhp2atnle  30844  lautcvr  30903  trlnidatb  30988  trlnid  30990  cdleme32e  31256  erng1lem  31798  erngdvlem4-rN  31810  diaelrnN  31857  diaf11N  31861  dibf11N  31973  cdlemn11pre  32022  dihord2pre  32037  dihord6apre  32068  dihvalrel  32091  dihglblem5apreN  32103  dihmeetlem13N  32131  mapdordlem2  32449  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  mapdheq2  32541
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 177
  Copyright terms: Public domain W3C validator