New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > an32s | GIF version |
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
Ref | Expression |
---|---|
an32s.1 | ⊢ (((φ ∧ ψ) ∧ χ) → θ) |
Ref | Expression |
---|---|
an32s | ⊢ (((φ ∧ χ) ∧ ψ) → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an32 773 | . 2 ⊢ (((φ ∧ χ) ∧ ψ) ↔ ((φ ∧ ψ) ∧ χ)) | |
2 | an32s.1 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) → θ) | |
3 | 1, 2 | sylbi 187 | 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: anass1rs 782 anabss1 787 ncfinlower 4483 nnadjoin 4520 nnpweq 4523 tfinnn 4534 fssres 5238 foco 5279 f1ores 5300 fun11iun 5305 fconstfv 5456 isocnv 5491 isomin 5496 f1oiso 5499 ncssfin 6151 nntccl 6170 tlecg 6230 ce2le 6233 nnc3n3p1 6278 nchoicelem12 6300 nchoicelem19 6307 |
Copyright terms: Public domain | W3C validator |