![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 527 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 119 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
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 |
This theorem is referenced by: anass1rs 536 anabss1 541 fssres 5134 foco 5190 fun11iun 5221 fconstfvm 5454 isocnv 5529 f1oiso 5543 f1ocnvfv3 5579 tfrcl 6060 mapxpen 6493 findcard 6533 exmidfodomrlemim 6729 genpassl 6985 genpassu 6986 cnegexlem3 7561 recexaplem2 8018 divap0 8048 dfinfre 8310 qreccl 9021 xrlttr 9159 addmodlteq 9693 cau3lem 10373 climcn1 10520 climcn2 10521 climcaucn 10561 rplpwr 10795 dvdssq 10799 nn0seqcvgd 10802 lcmgcdlem 10838 isprm6 10905 phiprmpw 10977 |
Copyright terms: Public domain | W3C validator |