![]() |
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 529 | . 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 538 anabss1 543 fssres 5186 foco 5243 fun11iun 5274 fconstfvm 5515 isocnv 5590 f1oiso 5605 f1ocnvfv3 5641 tfrcl 6129 mapxpen 6564 findcard 6604 exmidfodomrlemim 6827 genpassl 7083 genpassu 7084 cnegexlem3 7659 recexaplem2 8121 divap0 8151 dfinfre 8417 qreccl 9127 xrlttr 9265 addmodlteq 9805 cau3lem 10547 climcn1 10697 climcn2 10698 climcaucn 10740 rplpwr 11294 dvdssq 11298 nn0seqcvgd 11301 lcmgcdlem 11337 isprm6 11404 phiprmpw 11476 cncfco 11647 |
Copyright terms: Public domain | W3C validator |