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

Theorem syl22anc 1135
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (φψ)
sylXanc.2 (φχ)
sylXanc.3 (φθ)
sylXanc.4 (φτ)
syl22anc.5 (((ψ χ) (θ τ)) → η)
Assertion
Ref Expression
syl22anc (φη)

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3 (φψ)
2 sylXanc.2 . . 3 (φχ)
31, 2jca 290 . 2 (φ → (ψ χ))
4 sylXanc.3 . 2 (φθ)
5 sylXanc.4 . 2 (φτ)
6 syl22anc.5 . 2 (((ψ χ) (θ τ)) → η)
73, 4, 5, 6syl12anc 1132 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:  f1oprg  5111  tfrexlem  5889  th3qlem1  6144  ltanqg  6384  ltmnqg  6385  ltnnnq  6406  addcmpblnq0  6426  addlocprlemeqgt  6515  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  addcanprleml  6588  recexprlem1ssl  6605  caucvgprlemloc  6646  mulcmpblnr  6669  ltasrg  6698  recexgt0sr  6701  mulextsr1lem  6706  mulextsr1  6707  pitonnlem1p1  6742  axpre-ltadd  6770  mulgt0d  6934  mul4d  6965  add4d  6977  add42d  6978  subcan  7062  addsub4d  7165  subadd4d  7166  sub4d  7167  2addsubd  7168  addsubeq4d  7169  muladdd  7209  mulsubd  7210  addgegt0d  7306  addge0d  7308  le2addd  7349  le2subd  7350  ltleaddd  7351  leltaddd  7352  lt2subd  7354  apreap  7371  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  mulap0r  7399  mulge0d  7405  mulap0d  7421  divdivdivap  7471  divcanap5  7472  divap0d  7563  recdivapd  7564  recdivap2d  7565  divcanap6d  7566  ddcanapd  7567  rec11apd  7568  prodgt0  7599  lt2msq  7633  ledivdiv  7637  lediv12a  7641  recreclt  7647  divgt0d  7682  mulgt1d  7683  lemulge11d  7684  lemulge12d  7685  ltmul12ad  7688  lemul12ad  7689  lemul12bd  7690  nndivtr  7736  qreccl  8351  ledivdivd  8422  lediv12ad  8452  lt2mul2divd  8455  iccss2  8583  iccssico2  8586  lincmb01cmp  8641  iccf1o  8642  fzrev2i  8718  frecfzennn  8884  expcl2lemap  8921  mulexpzap  8949  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  ltexp2a  8960  leexp2a  8961  sqdivap  8972  expnbnd  9025  expsubapd  9045  lt2sqd  9064  le2sqd  9065  sq11d  9066  cjap  9134
  Copyright terms: Public domain W3C validator