New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 436 | . 2 ⊢ ((φ ∧ ψ) → (ψ ∧ φ)) | |
2 | pm3.22 436 | . 2 ⊢ ((ψ ∧ φ) → (φ ∧ ψ)) | |
3 | 1, 2 | impbii 180 | 1 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: ancomd 438 ancomsd 440 pm4.71r 612 pm5.32ri 619 pm5.32rd 621 anbi2ci 677 anbi12ci 679 an12 772 an32 773 an13 774 an42 798 andir 838 dfbi3 863 rbaib 873 rbaibr 874 3anrot 939 3ancoma 941 nancom 1290 excxor 1309 ancomsimp 1369 cador 1391 cadcoma 1395 cadcomb 1396 cad1 1398 exancom 1586 19.42 1880 eu1 2225 moaneu 2263 moanmo 2264 2eu3 2286 2eu6 2289 2eu7 2290 2eu8 2291 eq2tri 2412 r19.28av 2753 r19.29r 2755 r19.42v 2765 rexcomf 2770 rabswap 2790 euxfr2 3021 rmo4 3029 reu8 3032 rmo3 3133 incom 3448 difin2 3516 difin0ss 3616 ssunsn 3866 pw1in 4164 eluni1g 4172 elxpk2 4197 opkelcokg 4261 opkelimagekg 4271 cnvkxpk 4276 sikexlem 4295 dfpw12 4301 insklem 4304 unipw1 4325 addcass 4415 nnsucelrlem1 4424 nnsucelrlem2 4425 ltfinex 4464 ssfin 4470 dfop2lem1 4573 eqvinop 4606 opeq 4619 setconslem1 4731 setconslem2 4732 setconslem4 4734 elswap 4740 dfid3 4768 brinxp2 4835 brswap2 4860 cnvco 4894 dmuni 4914 dfima3 4951 elres 4995 dfres2 5002 imai 5010 rnuni 5038 cnvxp 5043 dmsnopg 5066 cnvsn 5073 rnco 5087 df2nd2 5111 fncnv 5158 fununi 5160 fnres 5199 fnopabg 5205 f1funfun 5263 dff1o2 5291 f1ocnvb 5298 eqfnfv3 5394 respreima 5410 fsn 5432 isoini 5497 opbr1st 5501 cnvswap 5510 swapf1o 5511 dmsi 5519 ndmovcom 5617 mptpreima 5682 trtxp 5781 brtxp 5783 elfix 5787 brimage 5793 oqelins4 5794 funsex 5828 pw1fnex 5852 clos1induct 5880 clos1is 5881 transex 5910 antisymex 5912 pmvalg 6010 elpmg 6013 mapval2 6018 enpw1lem1 6061 enmap2lem1 6063 enmap1lem1 6069 lecex 6115 ovmuc 6130 tcfnex 6244 addccan2nclem1 6263 nmembers1lem1 6268 nnc3n3p1 6278 spacvallem1 6281 spacis 6288 nchoicelem10 6298 nchoicelem11 6299 nchoicelem16 6304 |
Copyright terms: Public domain | W3C validator |