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 536 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | an32s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anass1rs 545 anabss1 550 fssres 5268 foco 5325 fun11iun 5356 fconstfvm 5606 isocnv 5680 f1oiso 5695 f1ocnvfv3 5731 tfrcl 6229 mapxpen 6710 findcard 6750 exmidfodomrlemim 7025 genpassl 7300 genpassu 7301 axsuploc 7805 cnegexlem3 7907 recexaplem2 8381 divap0 8412 dfinfre 8682 qreccl 9402 xrlttr 9549 addmodlteq 10139 cau3lem 10854 climcn1 11045 climcn2 11046 climcaucn 11088 rplpwr 11642 dvdssq 11646 nn0seqcvgd 11649 lcmgcdlem 11685 isprm6 11752 phiprmpw 11825 tgcl 12160 innei 12259 cncnp 12326 cnnei 12328 elbl2ps 12488 elbl2 12489 cncfco 12674 cnlimc 12737 |
Copyright terms: Public domain | W3C validator |