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

Theorem syl112anc 1174
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 300 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1170 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  fvun1  5265  reapmul1  7751  recrecap  7853  rec11rap  7855  divdivdivap  7857  dmdcanap  7866  ddcanap  7870  rerecclap  7874  div2negap  7879  divap1d  7944  divmulapd  7955  divmulap2d  7966  divmulap3d  7967  divassapd  7968  div12apd  7969  div23apd  7970  divdirapd  7971  divsubdirapd  7972  div11apd  7973  ltmul12a  7994  ltdiv1  8002  ltrec  8017  lt2msq1  8019  lediv2  8025  lediv23  8027  recp1lt1  8033  qapne  8794  modqge0  9403  modqlt  9404  modqid  9420  expgt1  9600  nnlesq  9664  expnbnd  9682  facubnd  9758  resqrexlemover  10023  mulcn2  10278  bezoutlemnewy  10518  bezoutlemstep  10519  mulgcd  10538  mulgcddvds  10609  prmind2  10635  oddpwdclemxy  10680  oddpwdclemodd  10683
  Copyright terms: Public domain W3C validator