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

Theorem syl2anc 391
Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
Hypotheses
Ref Expression
syl2anc.1 (φψ)
syl2anc.2 (φχ)
syl2anc.3 ((ψ χ) → θ)
Assertion
Ref Expression
syl2anc (φθ)

Proof of Theorem syl2anc
StepHypRef Expression
1 syl2anc.1 . 2 (φψ)
2 syl2anc.2 . 2 (φχ)
3 syl2anc.3 . . 3 ((ψ χ) → θ)
43ex 108 . 2 (ψ → (χθ))
51, 2, 4sylc 56 1 (φθ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  sylancl  392  sylancr  393  sylancom  397  mpdan  398  mpancom  399  orim12d  699  syl13anc  1136  syl31anc  1137  nford  1456  eqeq12d  2051  rsp2e  2366  r19.29d2r  2449  elrab3t  2691  eueq2dc  2708  csbiedf  2881  sstrd  2949  psstrd  3046  sspsstrd  3047  psssstrd  3048  uneq12d  3092  unssd  3113  ineq12d  3133  ssind  3155  preq12d  3446  opeq12d  3548  nfopd  3557  breq12d  3768  mpteq12dva  3829  ssexd  3888  exss  3954  opexg  3955  opth  3965  op1stbg  4176  tfisi  4253  xpeq12d  4313  poinxp  4352  eqbrrdv  4380  nfimad  4620  cnvexg  4798  funprg  4892  funtpg  4893  funimaexglem  4925  funfni  4942  fnunsn  4949  fnresdm  4951  fn0  4961  fssd  4998  fssxp  5001  fconstg  5026  fconst6g  5028  resdif  5091  nffvd  5130  sefvex  5139  feqresmpt  5170  fvelimab  5172  fvmptd  5196  fvmpt2d  5200  fvmptdf  5201  fvmptt  5205  eqfnfvd  5211  fnreseql  5220  fimacnv  5239  dff3im  5255  foco2  5261  ffvresb  5271  f1oresrab  5272  fmptco  5273  fmptapd  5297  fsnunf  5305  fconst3m  5323  fnex  5326  fcof1  5366  fcofo  5367  cocan1  5370  cocan2  5371  foeqcnvco  5373  f1eqcocnv  5374  fliftrel  5375  fliftel  5376  fliftel1  5377  fliftval  5383  isocnv2  5395  isores2  5396  isotr  5399  f1oiso2  5409  riotass2  5437  riotass  5438  oveq12d  5473  ovprc  5482  ovresd  5583  suppssov1  5651  offval  5661  ofrfval  5662  fnofval  5663  ofrval  5664  ofmresval  5665  offval2  5668  ofrfval2  5669  ofco  5671  caofinvl  5675  cofunexg  5680  fnexALT  5682  opabex3d  5690  oprabexd  5696  ofmresex  5706  xpopth  5744  eqop  5745  2nd1st  5748  2ndrn  5751  elopabi  5763  mpt2fvex  5771  oprab2co  5781  1stconst  5784  2ndconst  5785  cnvf1olem  5787  tposexg  5814  tposf2  5824  tposf12  5825  smoiso  5858  tfrlem1  5864  tfrlem5  5871  tfr0  5878  tfrlemisucaccv  5880  tfrlemibacc  5881  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  rdgivallem  5908  frecsuclem3  5929  frecrdg  5931  freccl  5932  sucinc2  5965  oav2  5982  omv2  5984  omsuc  5990  nnsucsssuc  6010  nnaordi  6017  nnaword  6020  nnmord  6026  nnmword  6027  nnaordex  6036  ercl  6053  ersym  6054  ertr  6057  swoer  6070  swoord1  6071  swoord2  6072  erth  6086  eroprf  6135  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  ecovicom  6150  ecoviass  6152  ecovidi  6154  f1oen2g  6171  fndmeng  6225  xpsnen2g  6239  xpdom1g  6243  xpdom3m  6244  fopwdom  6246  dfplpq2  6338  addcmpblnq  6351  addpipqqslem  6353  mulpipq2  6355  addcomnqg  6365  addassnqg  6366  distrnqg  6371  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltexnqq  6391  halfnqq  6393  subhalfnqq  6397  archnqq  6400  prarloclemarch  6401  prarloclemarch2  6402  ltrnqg  6403  enq0tr  6416  nqnq0pi  6420  addcmpblnq0  6425  nnnq0lem1  6428  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  distrnq0  6441  mulcomnq0  6442  addassnq0lemcl  6443  addassnq0  6444  preqlu  6454  prltlu  6469  prarloclemlt  6475  prarloclemlo  6476  prarloclem5  6482  prarloclemcalc  6484  prarloc  6485  genplt2i  6492  genpassg  6509  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemeqgt  6515  addlocprlemgt  6517  addlocprlem  6518  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  addnqpr1  6541  appdivnq  6542  prmuloclemcalc  6544  prmuloc  6545  prmuloc2  6546  mulnqprl  6547  mulnqpru  6548  mullocprlem  6549  mullocpr  6550  distrlem4prl  6558  distrlem4pru  6559  distrlem5prl  6560  distrlem5pru  6561  distrprg  6562  ltprordil  6563  1idprl  6564  1idpru  6565  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemlol  6574  ltexprlemopu  6575  ltexprlemupu  6576  ltexprlemloc  6579  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  ltexpri  6585  addcanprleml  6586  addcanprlemu  6587  ltaprlem  6589  ltaprg  6590  addextpr  6591  recexprlemm  6594  recexprlemdisj  6600  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  recexpr  6608  aptiprleml  6609  aptiprlemu  6610  ltmprr  6612  archpr  6613  addcmpblnr  6627  mulcmpblnrlemg  6628  mulcmpblnr  6629  prsrlem1  6630  ltsrprg  6635  mulcomsrg  6645  mulasssrg  6646  distrsrg  6647  lttrsr  6650  ltsosr  6652  ltasrg  6658  pn0sr  6659  negexsr  6660  recexgt0sr  6661  mulgt0sr  6664  aptisr  6665  mulextsr1lem  6666  mulextsr1  6667  archsr  6668  addcnsr  6691  mulcnsr  6692  addcnsrec  6699  mulcnsrec  6700  axaddcl  6710  axmulcl  6712  axmulcom  6715  axmulass  6717  axdistr  6718  axrnegex  6723  axcnre  6725  addcld  6804  mulcld  6805  mulcomd  6806  readdcld  6812  remulcld  6813  lelttr  6863  ltletr  6864  gtned  6887  lttri3d  6889  letri3d  6890  lenltd  6891  ltled  6892  readdcan  6910  addcomd  6921  cnegex  6946  negeu  6959  addsubass  6978  subsub2  6995  subsub4  7000  negcon1d  7072  neg11ad  7074  subcld  7078  pncand  7079  pncan2d  7080  pncan3d  7081  npcand  7082  nncand  7083  negsubd  7084  subnegd  7085  subeq0d  7086  subne0d  7087  subeq0ad  7088  negdid  7091  negdi2d  7092  negsubdid  7093  negsubdi2d  7094  neg2subd  7095  resubcld  7135  mulneg1d  7164  mulneg2d  7165  mul2negd  7166  ltadd2  7172  posdif  7205  add20  7224  ltnegd  7269  lenegd  7270  ltnegcon1d  7271  ltnegcon2d  7272  lenegcon1d  7273  lenegcon2d  7274  ltaddposd  7275  ltaddpos2d  7276  ltsubposd  7277  posdifd  7278  addge01d  7279  addge02d  7280  subge0d  7281  suble0d  7282  subge02d  7283  rimul  7329  rereim  7330  apreap  7331  reapmul1lem  7338  reapmul1  7339  reapadd1  7340  reapneg  7341  remulext1  7343  cru  7346  apreim  7347  apsym  7350  addext  7354  apneg  7355  mulext1  7356  mulext  7358  apti  7366  gt0ap0d  7371  recexaplem2  7375  recexap  7376  mulap0bd  7380  mulcanapd  7384  muleqadd  7391  receuap  7392  divmulap  7396  divdivdivap  7431  divcanap6  7437  recclapd  7499  recap0d  7500  recidapd  7501  recidap2d  7502  recrecapd  7503  dividapd  7504  div0apd  7505  rerecclapd  7548  recgt0  7557  prodgt0  7559  lt2msq  7593  lediv12a  7601  lediv2a  7602  recreclt  7607  recgt0d  7641  creui  7653  nnge1  7678  nnaddcld  7701  nnmulcld  7702  nndivred  7703  halfaddsub  7896  lt2halves  7897  addltmul  7898  nn0addcld  7975  nn0mulcld  7976  gtndiv  8071  zaddcld  8100  zsubcld  8101  zmulcld  8102  uzneg  8227  uzm1  8239  uzin  8241  uzind4  8267  qmulcl  8308  qapne  8310  rpaddcld  8372  rpmulcld  8373  rpdivcld  8374  ltrecd  8375  lerecd  8376  ltrec1d  8377  lerec2d  8378  ge0p1rpd  8383  rerpdivcld  8384  ltsubrpd  8385  ltaddrpd  8386  xrlelttr  8452  xrltletr  8453  ixxdisj  8502  ixxss1  8503  ixxss2  8504  iccsupr  8565  icoshft  8588  icoshftf1o  8589  icodisj  8590  elfz1eq  8629  fzen  8637  fzsplit  8645  elfz1end  8649  fznatpl1  8668  fzdifsuc  8673  uzdisj  8685  fseq1p1m1  8686  fzm1  8692  fzneuz  8693  fznuz  8694  uznfz  8695  fznn0sub2  8715  nn0disj  8725  elfzoelz  8734  elfzouz2  8747  fzonnsub  8755  fzospliti  8762  fzosplit  8763  fzodisj  8764  elfzo1  8776  eluzgtdifelfzo  8783  fzocatel  8785  zpnn0elfzo  8793  fzostep1  8823  frec2uzsucd  8828  frec2uzltd  8830  frec2uzlt2d  8831  frecuzrdgrrn  8835  frec2uzrdg  8836  frecuzrdgrom  8837  frecuzrdglem  8838  frecuzrdg0  8841  frecuzrdgsuc  8842  frecfzen2  8845  fzfig  8847  fzfigd  8848  iseqeq3  8856  iseqfveq2  8865  iseqfeq2  8866  expivallem  8870  expival  8871  expcl2lemap  8881  expap0  8899  expgt1  8907  mulexp  8908  mulexpzap  8909  expadd  8911  expaddzaplem  8912  expaddzap  8913  expmulzap  8915  ltexp2a  8920  leexp2a  8921  leexp2r  8922  bernneq  8982  expnbnd  8985  expnlbnd  8986  expnlbnd2  8987  expeq0d  8990  expcld  8994  expp1d  8995  sqrecapd  8998  sqmuld  9006  reexpcld  9011  nnexpcld  9015  nn0expcld  9016  rpexpcld  9017  sqgt0apd  9021  crre  9045  remim  9048  mulreap  9052  recj  9055  reneg  9056  readd  9057  remullem  9059  imcj  9063  imneg  9064  imadd  9065  cjexp  9081  cjap  9094  cjdivap  9097  cnrecnv  9098  cjexpd  9145  readdd  9146  imaddd  9147  resubd  9148  imsubd  9149  remuld  9150  immuld  9151  cjaddd  9152  cjmuld  9153  ipcnd  9154  remul2d  9159  immul2d  9160  crred  9163  crimd  9164  spimd  9174  bdssexd  9290
  Copyright terms: Public domain W3C validator