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

Theorem syl31anc 1251
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
sylXanc.4 (𝜑𝜏)
syl31anc.5 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl31anc (𝜑𝜂)

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1178 . 2 (𝜑 → (𝜓𝜒𝜃))
5 sylXanc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 411 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  syl32anc  1256  stoic4b  1443  enq0tr  7447  ltmul12a  8831  lt2msq1  8856  ledivp1  8874  lemul1ad  8910  lemul2ad  8911  lediv2ad  9733  xaddge0  9892  difelfznle  10149  expubnd  10591  nn0leexp2  10704  expcanlem  10709  expcand  10711  xrmaxaddlem  11282  mertenslemi1  11557  eftlub  11712  dvdsadd  11857  divalgmod  11946  gcdzeq  12037  rplpwr  12042  sqgcd  12044  bezoutr  12047  rpmulgcd2  12109  rpdvds  12113  isprm5  12156  divgcdodd  12157  oddpwdclemxy  12183  divnumden  12210  crth  12238  phimullem  12239  coprimeprodsq2  12272  pythagtriplem19  12296  pclemub  12301  pcpre1  12306  pcidlem  12336  pockthlem  12368  prmunb  12374  kerf1ghm  13168  xblss2ps  14257  xblss2  14258  metcnpi3  14370  limcimolemlt  14486  limccnp2cntop  14499  dvmulxxbr  14519  dvcoapbr  14524  2lgsoddprmlem1  14806  2sqlem8a  14822  2sqlem8  14823
  Copyright terms: Public domain W3C validator