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  7586  recrecap  7685  rec11rap  7687  divdivdivap  7689  dmdcanap  7698  ddcanap  7702  rerecclap  7706  div2negap  7711  divap1d  7776  divmulapd  7787  divmulap2d  7798  divmulap3d  7799  divassapd  7800  div12apd  7801  div23apd  7802  divdirapd  7803  divsubdirapd  7804  div11apd  7805  ltmul12a  7826  ltdiv1  7834  ltrec  7849  lt2msq1  7851  lediv2  7857  lediv23  7859  recp1lt1  7865  qapne  8574  modqge0  9174  modqlt  9175  expgt1  9293  nnlesq  9356  expnbnd  9372  resqrexlemover  9608  mulcn2  9833
  Copyright terms: Public domain W3C validator