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

Theorem syl22anc 1136
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 1133 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  5168  tfrexlem  5948  th3qlem1  6208  phplem4dom  6324  phplem4on  6329  fiunsnnn  6338  findcard2sd  6349  ltanqg  6498  ltmnqg  6499  ltnnnq  6521  addcmpblnq0  6541  addlocprlemeqgt  6630  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  addcanprleml  6712  recexprlem1ssl  6731  caucvgprlemloc  6773  caucvgprprlemloccalc  6782  mulcmpblnr  6826  ltasrg  6855  recexgt0sr  6858  mulextsr1lem  6864  mulextsr1  6865  srpospr  6867  prsrlt  6871  pitonnlem1p1  6922  recidpirq  6934  axpre-ltadd  6960  mulgt0d  7137  mul4d  7168  add4d  7180  add42d  7181  subcan  7266  addsub4d  7369  subadd4d  7370  sub4d  7371  2addsubd  7372  addsubeq4d  7373  muladdd  7413  mulsubd  7414  addgegt0d  7511  addge0d  7513  le2addd  7554  le2subd  7555  ltleaddd  7556  leltaddd  7557  lt2subd  7559  apreap  7578  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  mulap0r  7606  mulge0d  7612  mulap0d  7639  divdivdivap  7689  divcanap5  7690  divap0d  7781  recdivapd  7782  recdivap2d  7783  divcanap6d  7784  ddcanapd  7785  rec11apd  7786  divmuldivapd  7806  prodgt0  7818  lt2msq  7852  ledivdiv  7856  lediv12a  7860  recreclt  7866  divgt0d  7901  mulgt1d  7902  lemulge11d  7903  lemulge12d  7904  ltmul12ad  7907  lemul12ad  7908  lemul12bd  7909  nndivtr  7955  qreccl  8576  ledivdivd  8648  lediv12ad  8682  lt2mul2divd  8685  iccss2  8813  iccssico2  8816  lincmb01cmp  8871  iccf1o  8872  fzrev2i  8948  qtri3or  9098  2tnp1ge0ge0  9143  frecfzennn  9203  isermono  9237  expcl2lemap  9267  mulexpzap  9295  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  ltexp2a  9306  leexp2a  9307  sqdivap  9318  expnbnd  9372  expsubapd  9392  lt2sqd  9411  le2sqd  9412  sq11d  9413  cjap  9506  resqrexlem1arp  9603  resqrexlemp1rp  9604  resqrexlemglsq  9620  abs00ap  9660  absext  9661  absexpzap  9676  absrele  9679  sqrtmuld  9765  sqrtsq2d  9766  sqrtled  9767  sqrtltd  9768  sqr11d  9769  abs3lemd  9797  climuni  9814  2clim  9822  addcn2  9831  mulcn2  9833
  Copyright terms: Public domain W3C validator