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 552 | . 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 561 anabss1 566 fssres 5345 foco 5402 fun11iun 5435 fconstfvm 5685 isocnv 5761 f1oiso 5776 f1ocnvfv3 5813 tfrcl 6311 mapxpen 6793 findcard 6833 exmidfodomrlemim 7136 genpassl 7444 genpassu 7445 axsuploc 7950 cnegexlem3 8052 recexaplem2 8526 divap0 8557 dfinfre 8827 qreccl 9551 xrlttr 9702 addmodlteq 10297 cau3lem 11014 climcn1 11205 climcn2 11206 climcaucn 11248 ntrivcvgap 11445 rplpwr 11911 dvdssq 11915 nn0seqcvgd 11918 lcmgcdlem 11954 isprm6 12022 phiprmpw 12097 tgcl 12475 innei 12574 cncnp 12641 cnnei 12643 elbl2ps 12803 elbl2 12804 cncfco 12989 cnlimc 13052 |
Copyright terms: Public domain | W3C validator |