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

Theorem syl21anc 1171
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
syl21anc.4 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
syl21anc (𝜑𝜏)

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 302 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  issod  4119  brcogw  4572  funprg  5026  funtpg  5027  fnunsn  5083  ftpg  5438  fsnunf  5453  isotr  5550  off  5819  caofrss  5830  tfr1onlembxssdm  6056  tfrcllembxssdm  6069  pmresg  6379  ac6sfi  6560  tridc  6561  sbthlemi8  6610  casefun  6713  caseinj  6717  djufun  6721  djuinj  6723  mulclpi  6824  archnqq  6913  addlocprlemlt  7027  addlocprlemeq  7029  addlocprlemgt  7030  mullocprlem  7066  apreim  8014  ltrec1  8277  divge0d  9139  fseq1p1m1  9431  q2submod  9713  iseqoveq  9791  iseqcaopr2  9808  iseqdistr  9839  facavg  10043  shftfibg  10143  sqrtdiv  10363  sqrtdivd  10489  mulcn2  10586  dvdslegcd  10823  gcdnncl  10826  qredeu  10946  rpdvds  10948  rpexp  10999  oddpwdclemodd  11017  divnumden  11041  divdenle  11042  phimullem  11068
  Copyright terms: Public domain W3C validator