ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anc Unicode version

Theorem syl2anc 397
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
StepHypRef Expression
1 syl2anc.1 . 2  |-  ( ph  ->  ps )
2 syl2anc.2 . 2  |-  ( ph  ->  ch )
3 syl2anc.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
43ex 112 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 2, 4sylc 60 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  sylancl  398  sylancr  399  sylancom  405  mpdan  406  mpancom  407  orim12d  710  syl13anc  1148  syl31anc  1149  mp3an2i  1248  nford  1475  eqeq12d  2070  rsp2e  2389  r19.29d2r  2472  elrab3t  2720  eueq2dc  2737  csbiedf  2915  sstrd  2983  psstrd  3080  sspsstrd  3081  psssstrd  3082  uneq12d  3126  unssd  3147  ineq12d  3167  ssind  3189  preq12d  3483  opeq12d  3585  nfopd  3594  breq12d  3805  mpteq12dva  3866  ssexd  3925  exss  3991  opexg  3992  opth  4002  op1stbg  4238  onintexmid  4325  wetriext  4329  tfisi  4338  xpeq12d  4398  poinxp  4437  eqbrrdv  4465  nfimad  4705  cnvexg  4883  funprg  4977  funtpg  4978  funimaexglem  5010  funfni  5027  fnunsn  5034  fnresdm  5036  fn0  5046  fssd  5083  fssxp  5086  fconstg  5111  fconst6g  5113  resdif  5176  nffvd  5215  sefvex  5224  feqresmpt  5255  fvelimab  5257  fvmptd  5281  fvmpt2d  5285  fvmptdf  5286  fvmptt  5290  eqfnfvd  5296  fnreseql  5305  fimacnv  5324  dff3im  5340  foco2  5346  ffvresb  5356  f1oresrab  5357  fmptco  5358  fmptapd  5382  fsnunf  5390  fconst3m  5408  fnex  5411  fcof1  5451  fcofo  5452  cocan1  5455  cocan2  5456  foeqcnvco  5458  f1eqcocnv  5459  fliftrel  5460  fliftel  5461  fliftel1  5462  fliftval  5468  isocnv2  5480  isores2  5481  isotr  5484  f1oiso2  5494  riotass2  5522  riotass  5523  oveq12d  5558  ovexg  5567  ovprc  5568  ovresd  5669  suppssov1  5737  offval  5747  ofrfval  5748  fnofval  5749  ofrval  5750  ofmresval  5751  offval2  5754  ofrfval2  5755  ofco  5757  caofinvl  5761  cofunexg  5766  fnexALT  5768  opabex3d  5776  oprabexd  5782  ofmresex  5792  xpopth  5830  eqop  5831  2nd1st  5834  2ndrn  5837  elopabi  5849  mpt2fvex  5857  oprab2co  5867  1stconst  5870  2ndconst  5871  cnvf1olem  5873  tposexg  5904  tposf2  5914  tposf12  5915  smoiso  5948  tfrlem1  5954  tfrlem5  5961  tfr0  5968  tfrlemisucaccv  5970  tfrlemibacc  5971  tfrlemibxssdm  5972  tfrlemibfn  5973  tfrlemi14d  5978  tfrexlem  5979  rdgivallem  5999  frecsuclem3  6021  frecrdg  6023  freccl  6024  sucinc2  6057  oav2  6074  omv2  6076  omsuc  6082  nnsucsssuc  6102  nndifsnid  6111  nnaordi  6112  nnaword  6115  nnmord  6121  nnmword  6122  nnaordex  6131  ercl  6148  ersym  6149  ertr  6152  swoer  6165  swoord1  6166  swoord2  6167  erth  6181  eroprf  6230  ecopovtrn  6234  ecopovtrng  6237  th3qlem1  6239  ecovicom  6245  ecoviass  6247  ecovidi  6249  f1oen2g  6266  fndmeng  6320  xpsnen2g  6334  xpdom1g  6338  xpdom3m  6339  fopwdom  6341  phplem4dom  6355  phpm  6358  phplem4on  6360  fidceq  6361  fidifsnen  6362  dif1en  6368  fisbth  6371  diffisn  6381  diffifi  6382  ac6sfi  6383  fientri3  6384  nnwetri  6385  eqsupti  6402  supsnti  6409  supisolem  6412  supisoex  6413  ordiso2  6415  cardval3ex  6423  dfplpq2  6510  addcmpblnq  6523  addpipqqslem  6525  mulpipq2  6527  addcomnqg  6537  addassnqg  6538  distrnqg  6543  nqtri3or  6552  ltsonq  6554  ltanqg  6556  ltexnqq  6564  halfnqq  6566  subhalfnqq  6570  archnqq  6573  prarloclemarch  6574  prarloclemarch2  6575  ltrnqg  6576  enq0tr  6590  nqnq0pi  6594  addcmpblnq0  6599  nnnq0lem1  6602  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  distrnq0  6615  mulcomnq0  6616  addassnq0lemcl  6617  addassnq0  6618  preqlu  6628  prltlu  6643  prarloclemlt  6649  prarloclemlo  6650  prarloclem5  6656  prarloclemcalc  6658  prarloc  6659  genplt2i  6666  genpassg  6682  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  addlocprlemeqgt  6688  addlocprlemgt  6690  addlocprlem  6691  nqprl  6707  nqpru  6708  addnqprlemrl  6713  addnqprlemru  6714  addnqpr  6717  appdivnq  6719  prmuloclemcalc  6721  prmuloc  6722  prmuloc2  6723  mulnqprl  6724  mulnqpru  6725  mullocprlem  6726  mullocpr  6727  mulnqprlemrl  6729  mulnqprlemru  6730  mulnqpr  6733  distrlem4prl  6740  distrlem4pru  6741  distrlem5prl  6742  distrlem5pru  6743  distrprg  6744  ltprordil  6745  1idprl  6746  1idpru  6747  ltnqpri  6750  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemloc  6763  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  ltexpri  6769  addcanprleml  6770  addcanprlemu  6771  ltaprlem  6774  ltaprg  6775  prplnqu  6776  addextpr  6777  recexprlemm  6780  recexprlemdisj  6786  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  recexpr  6794  aptiprleml  6795  aptiprlemu  6796  ltmprr  6798  archpr  6799  caucvgprlemcanl  6800  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlemladd  6814  cauappcvgprlem1  6815  cauappcvgprlem2  6816  cauappcvgpr  6818  archrecpr  6820  caucvgprlemk  6821  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlemloc  6831  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprlem2  6836  caucvgpr  6838  caucvgprprlemk  6839  caucvgprprlemloccalc  6840  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  caucvgprprlemnkj  6848  caucvgprprlemnbj  6849  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlem1  6865  caucvgprprlem2  6866  caucvgprpr  6868  addcmpblnr  6882  mulcmpblnrlemg  6883  mulcmpblnr  6884  prsrlem1  6885  ltsrprg  6890  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  pn0sr  6914  negexsr  6915  recexgt0sr  6916  mulgt0sr  6920  aptisr  6921  mulextsr1lem  6922  mulextsr1  6923  archsr  6924  srpospr  6925  prsradd  6928  prsrlt  6929  prsrriota  6930  caucvgsrlemcl  6931  caucvgsrlemfv  6933  caucvgsrlemcau  6935  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsrlemofff  6939  caucvgsrlemoffcau  6940  caucvgsrlemoffgt1  6941  caucvgsrlemoffres  6942  addcnsr  6968  mulcnsr  6969  addcnsrec  6976  mulcnsrec  6977  ltrennb  6988  recidpipr  6990  recidpirqlemcalc  6991  recidpirq  6992  axaddcl  6998  axmulcl  7000  axmulcom  7003  axmulass  7005  axdistr  7006  axrnegex  7011  axcnre  7013  rereceu  7021  recriota  7022  nntopi  7026  axcaucvglemval  7029  axcaucvglemcau  7030  axcaucvglemres  7031  addcld  7104  mulcld  7105  mulcomd  7106  readdcld  7114  remulcld  7115  lelttr  7165  ltletr  7166  gtned  7189  lttri3d  7191  letri3d  7192  lenltd  7193  ltled  7194  readdcan  7214  addcomd  7225  cnegex  7252  negeu  7265  addsubass  7284  subsub2  7302  subsub4  7307  negcon1d  7379  neg11ad  7381  subcld  7385  pncand  7386  pncan2d  7387  pncan3d  7388  npcand  7389  nncand  7390  negsubd  7391  subnegd  7392  subeq0d  7393  subne0d  7394  subeq0ad  7395  negdid  7398  negdi2d  7399  negsubdid  7400  negsubdi2d  7401  neg2subd  7402  resubcld  7451  mulneg1d  7480  mulneg2d  7481  mul2negd  7482  ltadd2  7488  posdif  7524  add20  7543  ltnegd  7588  lenegd  7589  ltnegcon1d  7590  ltnegcon2d  7591  lenegcon1d  7592  lenegcon2d  7593  ltaddposd  7594  ltaddpos2d  7595  ltsubposd  7596  posdifd  7597  addge01d  7598  addge02d  7599  subge0d  7600  suble0d  7601  subge02d  7602  rimul  7650  rereim  7651  apreap  7652  reapmul1lem  7659  reapmul1  7660  reapadd1  7661  reapneg  7662  remulext1  7664  cru  7667  apreim  7668  apsym  7671  addext  7675  apneg  7676  mulext1  7677  mulext  7679  apti  7687  leltap  7689  gt0ap0d  7693  ltap  7696  ltapd  7701  ap0gt0d  7704  recexaplem2  7707  recexap  7708  mulap0bd  7712  mulcanapd  7716  muleqadd  7723  receuap  7724  divmulap  7728  divdivdivap  7764  divcanap6  7770  recclapd  7832  recap0d  7833  recidapd  7834  recidap2d  7835  recrecapd  7836  dividapd  7837  div0apd  7838  rerecclapd  7882  recgt0  7891  prodgt0  7893  lt2msq  7927  lediv12a  7935  lediv2a  7936  recreclt  7941  recgt0d  7975  creui  7988  nnge1  8013  nnaddcld  8037  nnmulcld  8038  nndivred  8039  halfaddsub  8216  lt2halves  8217  addltmul  8218  nn0addcld  8296  nn0mulcld  8297  gtndiv  8393  zaddcld  8423  zsubcld  8424  zmulcld  8425  uzneg  8587  uzm1  8599  uzin  8601  uzind4  8627  qmulcl  8669  qapne  8671  rpaddcld  8736  rpmulcld  8737  rpdivcld  8738  ltrecd  8739  lerecd  8740  ltrec1d  8741  lerec2d  8742  ge0p1rpd  8751  rerpdivcld  8752  ltsubrpd  8753  ltaddrpd  8754  xrlelttr  8823  xrltletr  8824  ixxdisj  8873  ixxss1  8874  ixxss2  8875  iccsupr  8936  icoshft  8959  icoshftf1o  8960  icodisj  8961  zltaddlt1le  8975  elfz1eq  9001  fzen  9009  fzsplit  9017  elfz1end  9021  fznatpl1  9040  fzdifsuc  9045  uzdisj  9057  fseq1p1m1  9058  fzm1  9064  fzneuz  9065  fznuz  9066  uznfz  9067  fznn0sub2  9087  nn0disj  9097  elfzoelz  9106  elfzouz2  9119  fzonnsub  9127  fzospliti  9134  fzosplit  9135  fzodisj  9136  elfzo1  9148  eluzgtdifelfzo  9155  fzocatel  9157  zpnn0elfzo  9165  fzostep1  9195  fvinim0ffz  9198  subfzo0  9199  qtri3or  9200  qbtwnzlemstep  9205  qbtwnz  9208  qbtwnre  9213  qavgle  9215  ico0  9218  flqlelt  9226  flqge  9232  flqlt  9233  flqwordi  9238  flqbi2  9241  fldivnn0  9245  flqaddz  9247  flqmulnn0  9249  flltdivnn0lt  9254  ceilqval  9256  intfracq  9270  flqdiv  9271  modqcl  9276  mulqmod0  9280  modqmulnn  9292  zmodcld  9295  modqcyc  9309  modqcyc2  9310  modqadd1  9311  mulqaddmodid  9314  mulp1mod1  9315  m1modnnsub1  9320  modqm1p1mod0  9325  modqltm1p1mod  9326  modqmul1  9327  q2submod  9335  modifeq2int  9336  modaddmodlo  9338  modqaddmulmod  9341  modqdi  9342  modqsubdir  9343  modsumfzodifsn  9346  addmodlteq  9348  frec2uzsucd  9351  frec2uzltd  9353  frec2uzlt2d  9354  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgrom  9360  frecuzrdglem  9361  frecuzrdg0  9364  frecuzrdgsuc  9365  frecfzen2  9368  fzfig  9370  fzfigd  9371  iseqeq3  9380  iseqm1  9391  iseqfveq2  9392  iseqfeq2  9393  iseqshft2  9396  monoord  9399  monoord2  9400  iseqsplit  9402  iseqcaopr3  9404  iseqid  9411  iseqhomo  9412  iseqz  9413  iseqdistr  9414  expivallem  9421  expival  9422  expcl2lemap  9432  expap0  9450  expgt1  9458  mulexp  9459  mulexpzap  9460  expadd  9462  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  ltexp2a  9472  leexp2a  9473  leexp2r  9474  mulbinom2  9533  bernneq  9537  expnbnd  9540  expnlbnd  9541  expnlbnd2  9542  expeq0d  9545  expcld  9549  expp1d  9550  sqrecapd  9553  sqmuld  9561  reexpcld  9566  nnexpcld  9571  nn0expcld  9572  rpexpcld  9573  sqgt0apd  9577  nn0opthlem1d  9588  nn0opthlem2d  9589  nn0opthd  9590  facwordi  9608  faclbnd  9609  faclbnd2  9610  faclbnd3  9611  faclbnd6  9612  facavg  9614  bcval  9617  bcval2  9618  bcrpcl  9621  bccmpl  9622  bcnp1n  9627  bcp1nk  9630  ibcval5  9631  bcp1m1  9633  bcpasc  9634  bccl2  9636  shftfvalg  9647  shftfval  9650  shftval2  9655  shftval5  9658  crre  9685  remim  9688  mulreap  9692  recj  9695  reneg  9696  readd  9697  remullem  9699  imcj  9703  imneg  9704  imadd  9705  cjexp  9721  cjap  9734  cjdivap  9737  cnrecnv  9738  cjexpd  9786  readdd  9787  imaddd  9788  resubd  9789  imsubd  9790  remuld  9791  immuld  9792  cjaddd  9793  cjmuld  9794  ipcnd  9795  remul2d  9800  immul2d  9801  crred  9804  crimd  9805  caucvgrelemcau  9807  caucvgre  9808  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniq  9822  resqrexlemover  9837  resqrexlemdecn  9839  resqrexlemcalc1  9841  resqrexlemcalc2  9842  resqrexlemnmsq  9844  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  resqrtcl  9856  rersqrtthlem  9857  sqrtmul  9862  rpsqrtcl  9868  sqrtdiv  9869  abscl  9878  absvalsq  9880  absge0  9887  abs00ap  9889  absreim  9895  absdivap  9897  leabs  9901  absexp  9906  absexpzap  9907  sqabs  9909  ltabs  9914  abslt  9915  absle  9916  abssubap0  9917  abssubne0  9918  absidm  9925  abssubge0  9929  abstri  9931  abs3dif  9932  abs2difabs  9935  fzomaxdiflem  9939  caubnd2  9944  amgm2  9945  absnidd  9987  resqrtcld  9990  sqrtmsqd  9991  sqrtsqd  9992  sqrtge0d  9993  absidd  9994  absltd  10001  absled  10002  absrpclapd  10015  absexpd  10019  abssubd  10020  absmuld  10021  abstrid  10023  abs2difd  10024  abs2dif2d  10025  abs2difabsd  10026  climconst  10042  climuni  10045  climmpt  10052  climshft  10056  climshft2  10058  climcn2  10061  mulcn2  10064  cn1lem  10065  cjcn2  10067  climrecl  10075  climle  10085  iserile  10093  climcau  10097  climcvg1nlem  10099  serif0  10102  dvdsval2  10111  moddvds  10117  dvds2lem  10120  iddvdsexp  10131  summodnegmod  10138  dvds2ln  10140  dvdsadd2b  10154  dvdslelemd  10155  dvdsle  10156  divconjdvds  10161  fzm1ndvds  10168  fzo0dvdseq  10169  fzocongeq  10170  dvdsfac  10172  dvdsexp  10173  dvdsmod  10174  mulmoddvds  10175  odd2np1lem  10183  odd2np1  10184  opeo  10209  omeo  10210  nn0o1gt2  10217  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  divalg  10236  divalgmod  10239  modremain  10241  fldivndvdslt  10247  pw2dvdslemn  10253  pw2dvds  10254  pw2dvdseulemle  10255  oddpwdclemxy  10257  oddpwdc  10262  nn0seqcvgd  10263  ialgr0  10266  ialgrp1  10268  ialgcvg  10270  algcvgb  10272  spimd  10292  bdssexd  10412  qdencn  10511
  Copyright terms: Public domain W3C validator