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  6508  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  addlocprlemeqgt  6514  addlocprlemgt  6516  addlocprlem  6517  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  addnqpr  6541  appdivnq  6543  prmuloclemcalc  6545  prmuloc  6546  prmuloc2  6547  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  mullocpr  6551  distrlem4prl  6559  distrlem4pru  6560  distrlem5prl  6561  distrlem5pru  6562  distrprg  6563  ltprordil  6564  1idprl  6565  1idpru  6566  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemloc  6580  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  ltexpri  6586  addcanprleml  6587  addcanprlemu  6588  ltaprlem  6590  ltaprg  6591  addextpr  6592  recexprlemm  6595  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  recexpr  6609  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  archpr  6614  cauappcvgprlemcan  6615  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlemladd  6629  cauappcvgprlem1  6630  cauappcvgprlem2  6631  cauappcvgpr  6633  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  prsrlem1  6650  ltsrprg  6655  mulcomsrg  6665  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltsosr  6672  ltasrg  6678  pn0sr  6679  negexsr  6680  recexgt0sr  6681  mulgt0sr  6684  aptisr  6685  mulextsr1lem  6686  mulextsr1  6687  archsr  6688  addcnsr  6711  mulcnsr  6712  addcnsrec  6719  mulcnsrec  6720  axaddcl  6730  axmulcl  6732  axmulcom  6735  axmulass  6737  axdistr  6738  axrnegex  6743  axcnre  6745  addcld  6824  mulcld  6825  mulcomd  6826  readdcld  6832  remulcld  6833  lelttr  6883  ltletr  6884  gtned  6907  lttri3d  6909  letri3d  6910  lenltd  6911  ltled  6912  readdcan  6930  addcomd  6941  cnegex  6966  negeu  6979  addsubass  6998  subsub2  7015  subsub4  7020  negcon1d  7092  neg11ad  7094  subcld  7098  pncand  7099  pncan2d  7100  pncan3d  7101  npcand  7102  nncand  7103  negsubd  7104  subnegd  7105  subeq0d  7106  subne0d  7107  subeq0ad  7108  negdid  7111  negdi2d  7112  negsubdid  7113  negsubdi2d  7114  neg2subd  7115  resubcld  7155  mulneg1d  7184  mulneg2d  7185  mul2negd  7186  ltadd2  7192  posdif  7225  add20  7244  ltnegd  7289  lenegd  7290  ltnegcon1d  7291  ltnegcon2d  7292  lenegcon1d  7293  lenegcon2d  7294  ltaddposd  7295  ltaddpos2d  7296  ltsubposd  7297  posdifd  7298  addge01d  7299  addge02d  7300  subge0d  7301  suble0d  7302  subge02d  7303  rimul  7349  rereim  7350  apreap  7351  reapmul1lem  7358  reapmul1  7359  reapadd1  7360  reapneg  7361  remulext1  7363  cru  7366  apreim  7367  apsym  7370  addext  7374  apneg  7375  mulext1  7376  mulext  7378  apti  7386  gt0ap0d  7391  recexaplem2  7395  recexap  7396  mulap0bd  7400  mulcanapd  7404  muleqadd  7411  receuap  7412  divmulap  7416  divdivdivap  7451  divcanap6  7457  recclapd  7519  recap0d  7520  recidapd  7521  recidap2d  7522  recrecapd  7523  dividapd  7524  div0apd  7525  rerecclapd  7568  recgt0  7577  prodgt0  7579  lt2msq  7613  lediv12a  7621  lediv2a  7622  recreclt  7627  recgt0d  7661  creui  7673  nnge1  7698  nnaddcld  7721  nnmulcld  7722  nndivred  7723  halfaddsub  7916  lt2halves  7917  addltmul  7918  nn0addcld  7995  nn0mulcld  7996  gtndiv  8091  zaddcld  8120  zsubcld  8121  zmulcld  8122  uzneg  8247  uzm1  8259  uzin  8261  uzind4  8287  qmulcl  8328  qapne  8330  rpaddcld  8392  rpmulcld  8393  rpdivcld  8394  ltrecd  8395  lerecd  8396  ltrec1d  8397  lerec2d  8398  ge0p1rpd  8403  rerpdivcld  8404  ltsubrpd  8405  ltaddrpd  8406  xrlelttr  8472  xrltletr  8473  ixxdisj  8522  ixxss1  8523  ixxss2  8524  iccsupr  8585  icoshft  8608  icoshftf1o  8609  icodisj  8610  elfz1eq  8649  fzen  8657  fzsplit  8665  elfz1end  8669  fznatpl1  8688  fzdifsuc  8693  uzdisj  8705  fseq1p1m1  8706  fzm1  8712  fzneuz  8713  fznuz  8714  uznfz  8715  fznn0sub2  8735  nn0disj  8745  elfzoelz  8754  elfzouz2  8767  fzonnsub  8775  fzospliti  8782  fzosplit  8783  fzodisj  8784  elfzo1  8796  eluzgtdifelfzo  8803  fzocatel  8805  zpnn0elfzo  8813  fzostep1  8843  frec2uzsucd  8848  frec2uzltd  8850  frec2uzlt2d  8851  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgrom  8857  frecuzrdglem  8858  frecuzrdg0  8861  frecuzrdgsuc  8862  frecfzen2  8865  fzfig  8867  fzfigd  8868  iseqeq3  8876  iseqfveq2  8885  iseqfeq2  8886  expivallem  8890  expival  8891  expcl2lemap  8901  expap0  8919  expgt1  8927  mulexp  8928  mulexpzap  8929  expadd  8931  expaddzaplem  8932  expaddzap  8933  expmulzap  8935  ltexp2a  8940  leexp2a  8941  leexp2r  8942  bernneq  9002  expnbnd  9005  expnlbnd  9006  expnlbnd2  9007  expeq0d  9010  expcld  9014  expp1d  9015  sqrecapd  9018  sqmuld  9026  reexpcld  9031  nnexpcld  9035  nn0expcld  9036  rpexpcld  9037  sqgt0apd  9041  crre  9065  remim  9068  mulreap  9072  recj  9075  reneg  9076  readd  9077  remullem  9079  imcj  9083  imneg  9084  imadd  9085  cjexp  9101  cjap  9114  cjdivap  9117  cnrecnv  9118  cjexpd  9165  readdd  9166  imaddd  9167  resubd  9168  imsubd  9169  remuld  9170  immuld  9171  cjaddd  9172  cjmuld  9173  ipcnd  9174  remul2d  9179  immul2d  9180  crred  9183  crimd  9184  spimd  9220  bdssexd  9336
  Copyright terms: Public domain W3C validator