![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ancom | GIF version |
Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.) |
Ref | Expression |
---|---|
ancom | ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 252 | . 2 ⊢ ((φ ∧ ψ) → (ψ ∧ φ)) | |
2 | pm3.22 252 | . 2 ⊢ ((ψ ∧ φ) → (φ ∧ ψ)) | |
3 | 1, 2 | impbii 117 | 1 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ancomd 254 ancomsd 256 pm4.71r 370 pm5.32rd 424 pm5.32ri 428 anbi2ci 432 anbi12ci 434 mpan10 443 an12 495 an32 496 an13 497 an42 521 andir 731 rbaib 829 rbaibr 830 3anrot 889 3ancoma 891 excxor 1268 xorcom 1276 xordc 1280 xordc1 1281 dfbi3dc 1285 ancomsimp 1326 exancom 1496 19.29r 1509 19.42h 1574 19.42 1575 eu1 1922 moaneu 1973 moanmo 1974 2eu7 1991 eq2tri 2096 r19.28av 2443 r19.29r 2445 r19.42v 2461 rexcomf 2466 rabswap 2482 euxfr2dc 2720 rmo4 2728 reu8 2731 rmo3 2843 incom 3123 difin2 3193 symdifxor 3197 inuni 3900 eqvinop 3971 uniuni 4149 dtruex 4237 elvvv 4346 brinxp2 4350 dmuni 4488 dfres2 4601 dfima2 4613 imadmrn 4621 imai 4624 cnvxp 4685 cnvcnvsn 4740 mptpreima 4757 rnco 4770 unixpm 4796 ressn 4801 xpcom 4807 fncnv 4908 fununi 4910 imadiflem 4921 fnres 4958 fnopabg 4965 dff1o2 5074 eqfnfv3 5210 respreima 5238 fsn 5278 fliftcnv 5378 isoini 5400 brtpos2 5807 tpostpos 5820 tposmpt2 5837 nnaord 6018 xpsnen 6231 xpcomco 6236 elni2 6298 enq0enq 6414 prltlu 6470 prnmaxl 6471 prnminu 6472 nqprrnd 6526 ltpopr 6569 letri3 6896 lesub0 7269 creur 7692 xrletri3 8491 iooneg 8626 iccneg 8627 elfzuzb 8654 fzrev 8716 redivap 9102 imdivap 9109 |
Copyright terms: Public domain | W3C validator |