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  addcmpblnq0  6425  addlocprlemeqgt  6514  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  addcanprleml  6587  recexprlem1ssl  6604  mulcmpblnr  6649  ltasrg  6678  recexgt0sr  6681  mulextsr1lem  6686  mulextsr1  6687  pitonnlem1p1  6722  axpre-ltadd  6750  mulgt0d  6914  mul4d  6945  add4d  6957  add42d  6958  subcan  7042  addsub4d  7145  subadd4d  7146  sub4d  7147  2addsubd  7148  addsubeq4d  7149  muladdd  7189  mulsubd  7190  addgegt0d  7286  addge0d  7288  le2addd  7329  le2subd  7330  ltleaddd  7331  leltaddd  7332  lt2subd  7334  apreap  7351  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  mulap0r  7379  mulge0d  7385  mulap0d  7401  divdivdivap  7451  divcanap5  7452  divap0d  7543  recdivapd  7544  recdivap2d  7545  divcanap6d  7546  ddcanapd  7547  rec11apd  7548  prodgt0  7579  lt2msq  7613  ledivdiv  7617  lediv12a  7621  recreclt  7627  divgt0d  7662  mulgt1d  7663  lemulge11d  7664  lemulge12d  7665  ltmul12ad  7668  lemul12ad  7669  lemul12bd  7670  nndivtr  7716  qreccl  8331  ledivdivd  8402  lediv12ad  8432  lt2mul2divd  8435  iccss2  8563  iccssico2  8566  lincmb01cmp  8621  iccf1o  8622  fzrev2i  8698  frecfzennn  8864  expcl2lemap  8901  mulexpzap  8929  expaddzaplem  8932  expaddzap  8933  expmulzap  8935  ltexp2a  8940  leexp2a  8941  sqdivap  8952  expnbnd  9005  expsubapd  9025  lt2sqd  9044  le2sqd  9045  sq11d  9046  cjap  9114
  Copyright terms: Public domain W3C validator