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  5155  tfrexlem  5935  th3qlem1  6195  phplem4dom  6311  phplem4on  6316  fiunsnnn  6325  findcard2sd  6335  ltanqg  6479  ltmnqg  6480  ltnnnq  6502  addcmpblnq0  6522  addlocprlemeqgt  6611  distrlem1prl  6661  distrlem1pru  6662  distrlem4prl  6663  distrlem4pru  6664  addcanprleml  6693  recexprlem1ssl  6712  caucvgprlemloc  6754  caucvgprprlemloccalc  6763  mulcmpblnr  6807  ltasrg  6836  recexgt0sr  6839  mulextsr1lem  6845  mulextsr1  6846  srpospr  6848  prsrlt  6852  pitonnlem1p1  6903  recidpirq  6915  axpre-ltadd  6941  mulgt0d  7117  mul4d  7148  add4d  7160  add42d  7161  subcan  7245  addsub4d  7348  subadd4d  7349  sub4d  7350  2addsubd  7351  addsubeq4d  7352  muladdd  7392  mulsubd  7393  addgegt0d  7489  addge0d  7491  le2addd  7532  le2subd  7533  ltleaddd  7534  leltaddd  7535  lt2subd  7537  apreap  7554  apsym  7573  apcotr  7574  apadd1  7575  apneg  7578  mulext1  7579  mulap0r  7582  mulge0d  7588  mulap0d  7615  divdivdivap  7665  divcanap5  7666  divap0d  7757  recdivapd  7758  recdivap2d  7759  divcanap6d  7760  ddcanapd  7761  rec11apd  7762  divmuldivapd  7782  prodgt0  7794  lt2msq  7828  ledivdiv  7832  lediv12a  7836  recreclt  7842  divgt0d  7877  mulgt1d  7878  lemulge11d  7879  lemulge12d  7880  ltmul12ad  7883  lemul12ad  7884  lemul12bd  7885  nndivtr  7931  qreccl  8547  ledivdivd  8619  lediv12ad  8649  lt2mul2divd  8652  iccss2  8780  iccssico2  8783  lincmb01cmp  8838  iccf1o  8839  fzrev2i  8915  frecfzennn  9081  isermono  9115  expcl2lemap  9145  mulexpzap  9173  expaddzaplem  9176  expaddzap  9177  expmulzap  9179  ltexp2a  9184  leexp2a  9185  sqdivap  9196  expnbnd  9250  expsubapd  9270  lt2sqd  9289  le2sqd  9290  sq11d  9291  cjap  9384  resqrexlem1arp  9481  resqrexlemp1rp  9482  resqrexlemglsq  9498  abs00ap  9538  absext  9539  absexpzap  9554  absrele  9557  sqrtmuld  9643  sqrtsq2d  9644  sqrtled  9645  sqrtltd  9646  sqr11d  9647  abs3lemd  9675  climuni  9691  2clim  9699  addcn2  9708  mulcn2  9710
  Copyright terms: Public domain W3C validator