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

Theorem syl112anc 1139
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 1135 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
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 887
This theorem is referenced by:  fvun1  5239  reapmul1  7584  recrecap  7683  rec11rap  7685  divdivdivap  7687  dmdcanap  7696  ddcanap  7700  rerecclap  7704  div2negap  7709  divap1d  7774  divmulapd  7785  divmulap2d  7796  divmulap3d  7797  divassapd  7798  div12apd  7799  div23apd  7800  divdirapd  7801  divsubdirapd  7802  div11apd  7803  ltmul12a  7824  ltdiv1  7832  ltrec  7847  lt2msq1  7849  lediv2  7855  lediv23  7857  recp1lt1  7863  qapne  8572  modqge0  9172  modqlt  9173  expgt1  9291  nnlesq  9354  expnbnd  9370  resqrexlemover  9606  mulcn2  9831
  Copyright terms: Public domain W3C validator