New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl22anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (φ → ψ) |
sylXanc.2 | ⊢ (φ → χ) |
sylXanc.3 | ⊢ (φ → θ) |
sylXanc.4 | ⊢ (φ → τ) |
syl22anc.5 | ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ)) → η) |
Ref | Expression |
---|---|
syl22anc | ⊢ (φ → η) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 ⊢ (φ → ψ) | |
2 | sylXanc.2 | . . 3 ⊢ (φ → χ) | |
3 | 1, 2 | jca 518 | . 2 ⊢ (φ → (ψ ∧ χ)) |
4 | sylXanc.3 | . 2 ⊢ (φ → θ) | |
5 | sylXanc.4 | . 2 ⊢ (φ → τ) | |
6 | syl22anc.5 | . 2 ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ)) → η) | |
7 | 3, 4, 5, 6 | syl12anc 1180 | 1 ⊢ (φ → η) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 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 |