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

Theorem syl31anc 1220
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 1162 . 2 (𝜑 → (𝜓𝜒𝜃))
5 sylXanc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 409 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  syl32anc  1225  stoic4b  1410  enq0tr  7265  ltmul12a  8641  lt2msq1  8666  ledivp1  8684  lemul1ad  8720  lemul2ad  8721  lediv2ad  9535  xaddge0  9690  difelfznle  9942  expubnd  10380  expcanlem  10492  expcand  10494  xrmaxaddlem  11060  mertenslemi1  11335  eftlub  11431  dvdsadd  11570  divalgmod  11658  gcdzeq  11744  rplpwr  11749  sqgcd  11751  bezoutr  11754  rpmulgcd2  11810  rpdvds  11814  divgcdodd  11855  oddpwdclemxy  11881  divnumden  11908  crth  11934  phimullem  11935  xblss2ps  12610  xblss2  12611  metcnpi3  12723  limcimolemlt  12839  limccnp2cntop  12852  dvmulxxbr  12872  dvcoapbr  12877
  Copyright terms: Public domain W3C validator