Theorem syl2anc 403

Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)

Hypotheses

Ref	Expression
syl2anc.1	|- ( ph -> ps )
syl2anc.2	|- ( ph -> ch )
syl2anc.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2anc	|- ( ph -> th )

Proof of Theorem syl2anc

Step	Hyp	Ref	Expression
1		syl2anc.1	. 2 |- ( ph -> ps )
2		syl2anc.2	. 2 |- ( ph -> ch )
3		syl2anc.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	3	ex 113	. 2 |- ( ps -> ( ch -> th ) )
5	1, 2, 4	sylc 61	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  sylancl  404  sylancr  405  sylancom  411  mpdan  412  mpancom  413  orim12d  732  syl13anc  1171  syl31anc  1172  mp3an2i  1273  nford  1499  eqeq12d  2095  rsp2e  2414  r19.29d2r  2499  elrab3t  2748  eueq2dc  2765  csbiedf  2943  sstrd  3009  uneq12d  3127  unssd  3148  ineq12d  3168  ssind  3190  preq12d  3477  opeq12d  3578  nfopd  3587  breq12d  3798  mpteq12dva  3859  ssexd  3918  exss  3982  opexg  3983  opth  3992  onintexmid  4315  wetriext  4319  tfisi  4328  xpeq12d  4388  poinxp  4427  eqbrrdv  4455  nfimad  4697  cnvexg  4875  funprg  4969  funtpg  4970  funimaexglem  5002  funfni  5019  fnunsn  5026  fnresdm  5028  fn0  5038  fssd  5075  fssxp  5078  fconstg  5103  fconst6g  5105  resdif  5168  nffvd  5207  sefvex  5216  feqresmpt  5248  fvelimab  5250  fvmptd  5274  fvmpt2d  5278  fvmptdf  5279  fvmptt  5283  eqfnfvd  5289  fnreseql  5298  fimacnv  5317  dff3im  5333  foco2  5339  ffvresb  5349  f1oresrab  5350  fmptco  5351  fmptapd  5375  fsnunf  5383  fconst3m  5401  fnex  5404  fcof1  5443  fcofo  5444  cocan1  5447  cocan2  5448  foeqcnvco  5450  f1eqcocnv  5451  fliftrel  5452  fliftel  5453  fliftel1  5454  fliftval  5460  isocnv2  5472  isores2  5473  isotr  5476  f1oiso2  5486  riotass2  5514  riotass  5515  oveq12d  5550  ovexg  5559  ovprc  5560  ovresd  5661  suppssov1  5729  offval  5739  ofrfval  5740  fnofval  5741  ofrval  5742  ofmresval  5743  offval2  5746  ofrfval2  5747  ofco  5749  caofinvl  5753  cofunexg  5758  fnexALT  5760  opabex3d  5768  oprabexd  5774  ofmresex  5784  xpopth  5822  eqop  5823  2nd1st  5826  2ndrn  5829  elopabi  5841  mpt2fvex  5849  oprab2co  5859  1stconst  5862  2ndconst  5863  cnvf1olem  5865  tposexg  5896  tposf2  5906  tposf12  5907  smoiso  5940  tfrlem1  5946  tfrlem5  5953  tfr0  5960  tfrlemisucaccv  5962  tfrlemibacc  5963  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemi14d  5970  tfrexlem  5971  rdgivallem  5991  frecsuclem3  6013  frecrdg  6015  freccl  6016  sucinc2  6049  oav2  6066  omv2  6068  omsuc  6074  nnsucsssuc  6094  nndifsnid  6103  nnaordi  6104  nnaword  6107  nnmord  6113  nnmword  6114  nnaordex  6123  ercl  6140  ersym  6141  ertr  6144  swoer  6157  swoord1  6158  swoord2  6159  erth  6173  eroprf  6222  ecopovtrn  6226  ecopovtrng  6229  th3qlem1  6231  ecovicom  6237  ecoviass  6239  ecovidi  6241  f1oen2g  6258  fndmeng  6312  xpsnen2g  6326  xpdom1g  6330  xpdom3m  6331  fopwdom  6333  phplem4dom  6348  phpm  6351  phplem4on  6353  fidceq  6354  fidifsnen  6355  dif1en  6364  fisbth  6367  diffisn  6377  diffifi  6378  ac6sfi  6379  en2eqpr  6380  fientri3  6381  nnwetri  6382  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  fnfi  6388  relcnvfi  6391  funrnfi  6392  f1dmvrnfibi  6393  eqsupti  6409  supsnti  6418  supisolem  6421  supisoex  6422  infglbti  6438  ordiso2  6446  cardval3ex  6454  dfplpq2  6544  addcmpblnq  6557  addpipqqslem  6559  mulpipq2  6561  addcomnqg  6571  addassnqg  6572  distrnqg  6577  nqtri3or  6586  ltsonq  6588  ltanqg  6590  ltexnqq  6598  halfnqq  6600  subhalfnqq  6604  archnqq  6607  prarloclemarch  6608  prarloclemarch2  6609  ltrnqg  6610  enq0tr  6624  nqnq0pi  6628  addcmpblnq0  6633  nnnq0lem1  6636  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  mulcomnq0  6650  addassnq0lemcl  6651  addassnq0  6652  preqlu  6662  prltlu  6677  prarloclemlt  6683  prarloclemlo  6684  prarloclem5  6690  prarloclemcalc  6692  prarloc  6693  genplt2i  6700  genpassg  6716  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  addlocprlemeqgt  6722  addlocprlemgt  6724  addlocprlem  6725  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  addnqpr  6751  appdivnq  6753  prmuloclemcalc  6755  prmuloc  6756  prmuloc2  6757  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqpr  6767  distrlem4prl  6774  distrlem4pru  6775  distrlem5prl  6776  distrlem5pru  6777  distrprg  6778  ltprordil  6779  1idprl  6780  1idpru  6781  ltnqpri  6784  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  ltexpri  6803  addcanprleml  6804  addcanprlemu  6805  ltaprlem  6808  ltaprg  6809  prplnqu  6810  addextpr  6811  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexpr  6828  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  archpr  6833  caucvgprlemcanl  6834  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlemladd  6848  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgpr  6852  archrecpr  6854  caucvgprlemk  6855  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemk  6873  caucvgprprlemloccalc  6874  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemnkj  6882  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgprpr  6902  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  prsrlem1  6919  ltsrprg  6924  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  pn0sr  6948  negexsr  6949  recexgt0sr  6950  mulgt0sr  6954  aptisr  6955  mulextsr1lem  6956  mulextsr1  6957  archsr  6958  srpospr  6959  prsradd  6962  prsrlt  6963  prsrriota  6964  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemofff  6973  caucvgsrlemoffcau  6974  caucvgsrlemoffgt1  6975  caucvgsrlemoffres  6976  addcnsr  7002  mulcnsr  7003  addcnsrec  7010  mulcnsrec  7011  ltrennb  7022  recidpipr  7024  recidpirqlemcalc  7025  recidpirq  7026  axaddcl  7032  axmulcl  7034  axmulcom  7037  axmulass  7039  axdistr  7040  axrnegex  7045  axcnre  7047  rereceu  7055  recriota  7056  nntopi  7060  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  addcld  7138  mulcld  7139  mulcomd  7140  readdcld  7148  remulcld  7149  lelttr  7199  ltletr  7200  gtned  7223  lttri3d  7225  letri3d  7226  lenltd  7227  ltled  7228  readdcan  7248  addcomd  7259  cnegex  7286  negeu  7299  addsubass  7318  subsub2  7336  subsub4  7341  negcon1d  7413  neg11ad  7415  subcld  7419  pncand  7420  pncan2d  7421  pncan3d  7422  npcand  7423  nncand  7424  negsubd  7425  subnegd  7426  subeq0d  7427  subne0d  7428  subeq0ad  7429  negdid  7432  negdi2d  7433  negsubdid  7434  negsubdi2d  7435  neg2subd  7436  resubcld  7485  negf1o  7486  mulneg1d  7515  mulneg2d  7516  mul2negd  7517  ltadd2  7523  posdif  7559  add20  7578  ltnegd  7623  lenegd  7624  ltnegcon1d  7625  ltnegcon2d  7626  lenegcon1d  7627  lenegcon2d  7628  ltaddposd  7629  ltaddpos2d  7630  ltsubposd  7631  posdifd  7632  addge01d  7633  addge02d  7634  subge0d  7635  suble0d  7636  subge02d  7637  rimul  7685  rereim  7686  apreap  7687  reapmul1lem  7694  reapmul1  7695  reapadd1  7696  reapneg  7697  remulext1  7699  cru  7702  apreim  7703  apsym  7706  addext  7710  apneg  7711  mulext1  7712  mulext  7714  apti  7722  leltap  7724  gt0ap0d  7728  ltap  7731  ltapd  7736  ap0gt0d  7739  recexaplem2  7742  recexap  7743  mulap0bd  7747  mulcanapd  7751  muleqadd  7758  receuap  7759  divmulap  7763  divdivdivap  7801  divcanap6  7807  recclapd  7869  recap0d  7870  recidapd  7871  recidap2d  7872  recrecapd  7873  dividapd  7874  div0apd  7875  rerecclapd  7919  recgt0  7928  prodgt0  7930  lt2msq  7964  lediv12a  7972  lediv2a  7973  recreclt  7978  recgt0d  8012  negiso  8033  creui  8037  nnge1  8062  nnaddcld  8086  nnmulcld  8087  nndivred  8088  halfaddsub  8265  lt2halves  8266  addltmul  8267  nn0addcld  8345  nn0mulcld  8346  gtndiv  8442  suprzclex  8445  zaddcld  8473  zsubcld  8474  zmulcld  8475  uzneg  8637  uzm1  8649  uzin  8651  uzind4  8676  supinfneg  8683  infsupneg  8684  supminfex  8685  qmulcl  8722  qapne  8724  rpaddcld  8789  rpmulcld  8790  rpdivcld  8791  ltrecd  8792  lerecd  8793  ltrec1d  8794  lerec2d  8795  ge0p1rpd  8804  rerpdivcld  8805  ltsubrpd  8806  ltaddrpd  8807  xrlelttr  8876  xrltletr  8877  ixxdisj  8926  ixxss1  8927  ixxss2  8928  iccsupr  8989  icoshft  9012  icoshftf1o  9013  icodisj  9014  zltaddlt1le  9028  elfz1eq  9054  fzen  9062  fzsplit  9070  elfz1end  9074  fznatpl1  9093  fzdifsuc  9098  uzdisj  9110  fseq1p1m1  9111  fzm1  9117  fzneuz  9118  fznuz  9119  uznfz  9120  fznn0sub2  9139  nn0disj  9148  elfzoelz  9157  elfzouz2  9170  fzonnsub  9178  fzospliti  9185  fzosplit  9186  fzodisj  9187  elfzo1  9199  eluzgtdifelfzo  9206  fzocatel  9208  zpnn0elfzo  9216  fzostep1  9246  exfzdc  9249  fvinim0ffz  9250  subfzo0  9251  qtri3or  9252  qbtwnzlemstep  9257  qbtwnz  9260  qbtwnre  9265  qavgle  9267  ico0  9270  flqlelt  9278  flqge  9284  flqlt  9285  flqwordi  9290  flqbi2  9293  fldivnn0  9297  flqaddz  9299  flqmulnn0  9301  flltdivnn0lt  9306  ceilqval  9308  intfracq  9322  flqdiv  9323  modqcl  9328  mulqmod0  9332  modqmulnn  9344  zmodcld  9347  modqcyc  9361  modqcyc2  9362  modqadd1  9363  mulqaddmodid  9366  mulp1mod1  9367  m1modnnsub1  9372  modqm1p1mod0  9377  modqltm1p1mod  9378  modqmul1  9379  q2submod  9387  modifeq2int  9388  modaddmodlo  9390  modqaddmulmod  9393  modqdi  9394  modqsubdir  9395  modsumfzodifsn  9398  addmodlteq  9400  frec2uzsucd  9403  frec2uzltd  9405  frec2uzlt2d  9406  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgrom  9412  frecuzrdglem  9413  frecuzrdg0  9416  frecuzrdgsuc  9417  frecfzen2  9420  fzfig  9422  fzfigd  9423  uzsinds  9428  iseqeq3  9436  iseqm1  9447  iseqfveq2  9448  iseqfeq2  9449  iseqshft2  9452  monoord  9455  monoord2  9456  iseqsplit  9458  iseqcaopr3  9460  iseqid  9467  iseqhomo  9468  iseqz  9469  iseqdistr  9470  expivallem  9477  expival  9478  expcl2lemap  9488  expap0  9506  expgt1  9514  mulexp  9515  mulexpzap  9516  expadd  9518  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  ltexp2a  9528  leexp2a  9529  leexp2r  9530  mulbinom2  9589  bernneq  9593  expnbnd  9596  expnlbnd  9597  expnlbnd2  9598  expeq0d  9601  expcld  9605  expp1d  9606  sqrecapd  9609  sqmuld  9617  reexpcld  9622  nnexpcld  9627  nn0expcld  9628  rpexpcld  9629  sqgt0apd  9633  nn0opthlem1d  9647  nn0opthlem2d  9648  nn0opthd  9649  facwordi  9667  faclbnd  9668  faclbnd2  9669  faclbnd3  9670  faclbnd6  9671  facavg  9673  bcval  9676  bcval2  9677  bcrpcl  9680  bccmpl  9681  bcnp1n  9686  bcp1nk  9689  ibcval5  9690  bcp1m1  9692  bcpasc  9693  bccl2  9695  shftfvalg  9706  shftfval  9709  shftval2  9714  shftval5  9717  crre  9744  remim  9747  mulreap  9751  recj  9754  reneg  9755  readd  9756  remullem  9758  imcj  9762  imneg  9763  imadd  9764  cjexp  9780  cjap  9793  cjdivap  9796  cnrecnv  9797  cjexpd  9845  readdd  9846  imaddd  9847  resubd  9848  imsubd  9849  remuld  9850  immuld  9851  cjaddd  9852  cjmuld  9853  ipcnd  9854  remul2d  9859  immul2d  9860  crred  9863  crimd  9864  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemnmsq  9903  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrtcl  9915  rersqrtthlem  9916  sqrtmul  9921  rpsqrtcl  9927  sqrtdiv  9928  abscl  9937  absvalsq  9939  absge0  9946  abs00ap  9948  absreim  9954  absdivap  9956  leabs  9960  absexp  9965  absexpzap  9966  sqabs  9968  ltabs  9973  abslt  9974  absle  9975  abssubap0  9976  abssubne0  9977  absidm  9984  abssubge0  9988  abstri  9990  abs3dif  9991  abs2difabs  9994  fzomaxdiflem  9998  caubnd2  10003  amgm2  10004  absnidd  10046  resqrtcld  10049  sqrtmsqd  10050  sqrtsqd  10051  sqrtge0d  10052  absidd  10053  absltd  10060  absled  10061  absrpclapd  10074  absexpd  10078  abssubd  10079  absmuld  10080  abstrid  10082  abs2difd  10083  abs2dif2d  10084  abs2difabsd  10085  maxabslemlub  10093  maxleastb  10100  maxltsup  10104  fimaxre2  10109  negfi  10110  minmax  10112  lemininf  10115  ltmininf  10116  climconst  10129  climuni  10132  climmpt  10139  climshft  10143  climshft2  10145  climcn2  10148  mulcn2  10151  cn1lem  10152  cjcn2  10154  climrecl  10162  climle  10172  iserile  10180  climcau  10184  climcvg1nlem  10186  serif0  10189  dvdsval2  10198  moddvds  10204  dvds2lem  10207  zdvdsdc  10216  iddvdsexp  10219  summodnegmod  10226  dvds2ln  10228  dvdsadd2b  10242  dvdslelemd  10243  dvdsle  10244  divconjdvds  10249  fzm1ndvds  10256  fzo0dvdseq  10257  fzocongeq  10258  dvdsfac  10260  dvdsexp  10261  dvdsmod  10262  mulmoddvds  10263  odd2np1lem  10271  odd2np1  10272  opeo  10297  omeo  10298  nn0o1gt2  10305  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  divalg  10324  divalgmod  10327  modremain  10329  fldivndvdslt  10335  zsupcl  10343  zssinfcl  10344  infssuzex  10345  dvdsbnd  10348  nndvdslegcd  10357  gcdcld  10360  zeqzmulgcd  10362  divgcdnn  10366  gcdn0gt0  10369  gcdaddm  10375  modgcd  10382  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlemeu  10396  bezoutlemle  10397  dfgcd3  10399  bezout  10400  dvdsgcd  10401  dfgcd2  10403  gcdass  10404  mulgcd  10405  gcddiv  10408  gcdmultiple  10409  gcdmultiplez  10410  gcdzeq  10411  dvdsmulgcd  10414  rplpwr  10416  rppwr  10417  sqgcd  10418  bezoutr1  10422  nn0seqcvgd  10423  ialgr0  10426  ialgrp1  10428  ialgcvg  10430  algcvgb  10432  eucalgval2  10435  eucalgval  10436  eucalgf  10437  eucalginv  10438  eucalglt  10439  lcmval  10445  lcmcllem  10449  lcmledvds  10452  lcmneg  10456  lcmgcdlem  10459  lcmass  10467  ncoprmgcdne1b  10471  coprmdvds2  10475  mulgcddvds  10476  rpmulgcd2  10477  qredeu  10479  rpdvds  10481  congr  10482  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  1idssfct  10497  isprm4  10501  prmind2  10502  dvdsnprmd  10507  oddprmge3  10516  sqnprm  10517  exprmfct  10519  coprm  10523  euclemma  10525  isprm6  10526  prmexpb  10530  prmfac1  10531  rpexp  10532  rpexp12i  10534  pw2dvdslemn  10543  pw2dvds  10544  pw2dvdseulemle  10545  oddpwdclemxy  10547  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  znege1  10556  sqrt2irraplemnn  10557  sqrt2irrap  10558  spimd  10576  bdssexd  10696  qdencn  10785