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  7339  recrecap  7427  rec11rap  7429  divdivdivap  7431  dmdcanap  7440  ddcanap  7444  rerecclap  7448  div2negap  7453  divap1d  7518  divmulapd  7529  divmulap2d  7540  divmulap3d  7541  divassapd  7542  div12apd  7543  div23apd  7544  divdirapd  7545  divsubdirapd  7546  div11apd  7547  ltmul12a  7567  ltdiv1  7575  ltrec  7590  lt2msq1  7592  lediv2  7598  lediv23  7600  recp1lt1  7606  qapne  8310  expgt1  8907  nnlesq  8969  expnbnd  8985
  Copyright terms: Public domain W3C validator