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

Theorem syl22anc 1173
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 300 . 2 (𝜑 → (𝜓𝜒))
4 sylXanc.3 . 2 (𝜑𝜃)
5 sylXanc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 1170 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  f1oprg  5260  tfrexlem  6055  th3qlem1  6348  ssenen  6521  phplem4dom  6532  phplem4on  6537  fiunsnnn  6551  findcard2sd  6562  unsnfi  6583  sbthlemi9  6621  ltanqg  6906  ltmnqg  6907  ltnnnq  6929  addcmpblnq0  6949  addlocprlemeqgt  7038  distrlem1prl  7088  distrlem1pru  7089  distrlem4prl  7090  distrlem4pru  7091  addcanprleml  7120  recexprlem1ssl  7139  caucvgprlemloc  7181  caucvgprprlemloccalc  7190  mulcmpblnr  7234  ltasrg  7263  recexgt0sr  7266  mulextsr1lem  7272  mulextsr1  7273  srpospr  7275  prsrlt  7279  pitonnlem1p1  7330  recidpirq  7342  axpre-ltadd  7368  mulgt0d  7553  mul4d  7584  add4d  7598  add42d  7599  subcan  7684  addsub4d  7787  subadd4d  7788  sub4d  7789  2addsubd  7790  addsubeq4d  7791  muladdd  7841  mulsubd  7842  addgegt0d  7941  addge0d  7943  le2addd  7984  le2subd  7985  ltleaddd  7986  leltaddd  7987  lt2subd  7989  apreap  8008  apsym  8027  apcotr  8028  apadd1  8029  apneg  8032  mulext1  8033  mulap0r  8036  mulge0d  8042  mulap0d  8069  divdivdivap  8122  divcanap5  8123  divap0d  8214  recdivapd  8215  recdivap2d  8216  divcanap6d  8217  ddcanapd  8218  rec11apd  8219  divmuldivapd  8239  prodgt0  8251  lt2msq  8285  ledivdiv  8289  lediv12a  8293  recreclt  8299  divgt0d  8334  mulgt1d  8335  lemulge11d  8336  lemulge12d  8337  ltmul12ad  8340  lemul12ad  8341  lemul12bd  8342  nndivtr  8401  qreccl  9062  ledivdivd  9134  lediv12ad  9168  lt2mul2divd  9171  iccss2  9297  iccssico2  9300  lincmb01cmp  9355  iccf1o  9356  fzrev2i  9433  qtri3or  9585  2tnp1ge0ge0  9639  modqid  9687  q0mod  9693  q1mod  9694  modqabs  9695  modqadd1  9699  mulqaddmodid  9702  mulp1mod1  9703  modqmuladd  9704  modqmuladdnn0  9706  qnegmod  9707  m1modnnsub1  9708  addmodid  9710  modqm1p1mod0  9713  modqltm1p1mod  9714  modqmul1  9715  q2submod  9723  modifeq2int  9724  modaddmodup  9725  modaddmodlo  9726  modqaddmulmod  9729  modqsubdir  9731  modqeqmodmin  9732  modsumfzodifsn  9734  addmodlteq  9736  frecfzennn  9764  isermono  9815  expcl2lemap  9869  mulexpzap  9897  expaddzaplem  9900  expaddzap  9901  expmulzap  9903  ltexp2a  9909  leexp2a  9910  sqdivap  9921  expnbnd  9977  expsubapd  9997  lt2sqd  10017  le2sqd  10018  sq11d  10019  bcp1nk  10070  hashunlem  10112  zfz1isolem1  10145  cjap  10239  resqrexlem1arp  10337  resqrexlemp1rp  10338  resqrexlemglsq  10354  abs00ap  10394  absext  10395  absexpzap  10412  absrele  10415  sqrtmuld  10501  sqrtsq2d  10502  sqrtled  10503  sqrtltd  10504  sqr11d  10505  abs3lemd  10533  minmax  10559  climuni  10579  2clim  10587  addcn2  10596  mulcn2  10598  fisum  10670  dvds1  10760  dvdsext  10762  mulmoddvds  10770  oexpneg  10783  evennn02n  10788  evennn2n  10789  bezoutlemmo  10901  mulgcd  10911  dvdssqlem  10925  rpmulgcd2  10983  isprm6  11032  sqrt2irraplemnn  11063  sqrt2irrap  11064  crth  11106  unennn  11116
  Copyright terms: Public domain W3C validator