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

Theorem syl31anc 1173
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 1119 . 2 (𝜑 → (𝜓𝜒𝜃))
5 sylXanc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 403 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  syl32anc  1178  stoic4b  1363  enq0tr  6722  ltmul12a  8041  lt2msq1  8066  ledivp1  8084  lemul1ad  8120  lemul2ad  8121  lediv2ad  8913  difelfznle  9259  expubnd  9666  expcanlem  9776  expcand  9778  dvdsadd  10430  divalgmod  10518  gcdzeq  10602  rplpwr  10607  sqgcd  10609  bezoutr  10612  rpmulgcd2  10668  rpdvds  10672  divgcdodd  10713  oddpwdclemxy  10738  divnumden  10765  crth  10791  phimullem  10792
  Copyright terms: Public domain W3C validator