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

Theorem syl112anc 1185
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 301 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1181 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  fvun1  5405  caseinl  6862  reapmul1  8169  recrecap  8273  rec11rap  8275  divdivdivap  8277  dmdcanap  8286  ddcanap  8290  rerecclap  8294  div2negap  8299  divap1d  8365  divmulapd  8376  apdivmuld  8377  divmulap2d  8388  divmulap3d  8389  divassapd  8390  div12apd  8391  div23apd  8392  divdirapd  8393  divsubdirapd  8394  div11apd  8395  ltmul12a  8418  ltdiv1  8426  ltrec  8441  lt2msq1  8443  lediv2  8449  lediv23  8451  recp1lt1  8457  qapne  9223  xadd4d  9451  xleaddadd  9453  modqge0  9888  modqlt  9889  modqid  9905  expgt1  10124  nnlesq  10189  expnbnd  10208  facubnd  10284  resqrexlemover  10574  mulcn2  10871  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  eftlub  11145  eflegeo  11157  sin01bnd  11213  cos01bnd  11214  eirraplem  11229  bezoutlemnewy  11428  bezoutlemstep  11429  mulgcd  11448  mulgcddvds  11519  prmind2  11545  oddpwdclemxy  11590  oddpwdclemodd  11593  qnumgt0  11619  xblm  12219
  Copyright terms: Public domain W3C validator