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 263 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) | |
2 | pm3.22 263 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓)) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 |
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: ancomd 265 ancomsd 267 biancomi 268 biancomd 269 pm4.71r 388 pm5.32rd 447 pm5.32ri 451 anbi2ci 455 anbi12ci 457 mpan10 466 an12 551 an32 552 an13 553 an42 577 andir 809 rbaib 911 rbaibr 912 3anrot 972 3ancoma 974 excxor 1367 xorcom 1377 xordc 1381 xordc1 1382 dfbi3dc 1386 ancomsimp 1427 exancom 1595 19.29r 1608 19.42h 1674 19.42 1675 eu1 2038 moaneu 2089 moanmo 2090 2eu7 2107 eq2tri 2224 r19.28av 2600 r19.29r 2602 r19.42v 2621 rexcomf 2626 rabswap 2642 euxfr2dc 2906 rmo4 2914 reu8 2917 rmo3f 2918 rmo3 3037 incom 3309 difin2 3379 symdifxor 3383 inuni 4128 eqvinop 4215 uniuni 4423 dtruex 4530 elvvv 4661 brinxp2 4665 dmuni 4808 dfres2 4930 dfima2 4942 imadmrn 4950 imai 4954 cnvxp 5016 cnvcnvsn 5074 mptpreima 5091 rnco 5104 unixpm 5133 ressn 5138 xpcom 5144 fncnv 5248 fununi 5250 imadiflem 5261 fnres 5298 fnopabg 5305 dff1o2 5431 eqfnfv3 5579 respreima 5607 fsn 5651 fliftcnv 5757 isoini 5780 spc2ed 6192 brtpos2 6210 tpostpos 6223 tposmpo 6240 nnaord 6468 pmex 6610 elpmg 6621 mapval2 6635 mapsnen 6768 map1 6769 xpsnen 6778 xpcomco 6783 elfi2 6928 supmoti 6949 cnvti 6975 elni2 7246 enq0enq 7363 prltlu 7419 prnmaxl 7420 prnminu 7421 nqprrnd 7475 ltpopr 7527 letri3 7970 lesub0 8368 creur 8845 xrletri3 9731 iooneg 9915 iccneg 9916 elfzuzb 9945 fzrev 10009 redivap 10802 imdivap 10809 rersqreu 10956 lenegsq 11023 climrecvg1n 11275 fisumcom2 11365 fsumcom 11366 fprodcom2fi 11553 fprodcom 11554 gcdcom 11891 bezoutlembi 11923 dfgcd2 11932 lcmcom 11975 isprm2 12028 unennn 12273 ntreq0 12679 restopn2 12730 ismet2 12901 blres 12981 metrest 13053 dedekindicclemicc 13157 sincosq3sgn 13296 |
Copyright terms: Public domain | W3C validator |