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

Theorem syl112anc 1138
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (φψ)
sylXanc.2 (φχ)
sylXanc.3 (φθ)
sylXanc.4 (φτ)
syl112anc.5 ((ψ χ (θ τ)) → η)
Assertion
Ref Expression
syl112anc (φη)

Proof of Theorem syl112anc
StepHypRef Expression
1 sylXanc.1 . 2 (φψ)
2 sylXanc.2 . 2 (φχ)
3 sylXanc.3 . . 3 (φθ)
4 sylXanc.4 . . 3 (φτ)
53, 4jca 290 . 2 (φ → (θ τ))
6 syl112anc.5 . 2 ((ψ χ (θ τ)) → η)
71, 2, 5, 6syl3anc 1134 1 (φη)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  fvun1  5182  reapmul1  7359  recrecap  7447  rec11rap  7449  divdivdivap  7451  dmdcanap  7460  ddcanap  7464  rerecclap  7468  div2negap  7473  divap1d  7538  divmulapd  7549  divmulap2d  7560  divmulap3d  7561  divassapd  7562  div12apd  7563  div23apd  7564  divdirapd  7565  divsubdirapd  7566  div11apd  7567  ltmul12a  7587  ltdiv1  7595  ltrec  7610  lt2msq1  7612  lediv2  7618  lediv23  7620  recp1lt1  7626  qapne  8330  expgt1  8927  nnlesq  8989  expnbnd  9005
  Copyright terms: Public domain W3C validator