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

Theorem syl31anc 1187
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 1129 . 2 (𝜑 → (𝜓𝜒𝜃))
5 sylXanc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 406 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  syl32anc  1192  stoic4b  1377  enq0tr  7143  ltmul12a  8476  lt2msq1  8501  ledivp1  8519  lemul1ad  8555  lemul2ad  8556  lediv2ad  9353  xaddge0  9502  difelfznle  9753  expubnd  10191  expcanlem  10303  expcand  10305  xrmaxaddlem  10868  mertenslemi1  11143  eftlub  11194  dvdsadd  11331  divalgmod  11419  gcdzeq  11503  rplpwr  11508  sqgcd  11510  bezoutr  11513  rpmulgcd2  11569  rpdvds  11573  divgcdodd  11614  oddpwdclemxy  11639  divnumden  11666  crth  11692  phimullem  11693  xblss2ps  12332  xblss2  12333  metcnpi3  12441  limcimolemlt  12513
  Copyright terms: Public domain W3C validator