New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl22anc GIF version

Theorem syl22anc 1183
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (φψ)
sylXanc.2 (φχ)
sylXanc.3 (φθ)
sylXanc.4 (φτ)
syl22anc.5 (((ψ χ) (θ τ)) → η)
Assertion
Ref Expression
syl22anc (φη)

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3 (φψ)
2 sylXanc.2 . . 3 (φχ)
31, 2jca 518 . 2 (φ → (ψ χ))
4 sylXanc.3 . 2 (φθ)
5 sylXanc.4 . 2 (φτ)
6 syl22anc.5 . 2 (((ψ χ) (θ τ)) → η)
73, 4, 5, 6syl12anc 1180 1 (φη)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  prepeano4  4451  preaddccan2  4455  ncfindi  4475  ncfinsn  4476  ncfineleq  4477  nnpw1ex  4484  tfin11  4493  tfinpw1  4494  ncfintfin  4495  tfindi  4496  tfinsuc  4498  evenodddisj  4516  sfin112  4529  vfintle  4546  vfinspsslem1  4550  vfinncsp  4554  enadj  6060  ncdisjun  6136  nntccl  6170  ceclnn1  6189  sbth  6206  tcncg  6224  cet  6234  spacis  6288  nchoicelem6  6294
 Copyright terms: Public domain W3C validator