![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biancomi | Structured version Visualization version GIF version |
Description: Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.) |
Ref | Expression |
---|---|
biancomi.1 | ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓)) |
Ref | Expression |
---|---|
biancomi | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biancomi.1 | . 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓)) | |
2 | ancom 460 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
3 | 1, 2 | bitr4i 278 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: biantrur 530 rbaibr 537 pm4.71ri 560 anbi2ci 624 anbi1ci 625 anbi12ci 628 an12 644 an32 645 mpbiran2 709 eu6lem 2576 elon2 6406 fununi 6653 fnopabg 6717 eqfnfv3 7066 respreima 7099 fsn 7169 brtpos2 8273 tpostpos 8287 oeeu 8659 mapval2 8930 xrltlen 13208 ssfzoulel 13810 xpcogend 15023 dfgcd2 16593 isffth2 17983 resscntz 19373 fiidomfld 20797 1stcelcls 23490 txflf 24035 fclsrest 24053 tsmssubm 24172 blres 24462 xrtgioo 24847 isncvsngp 25202 itg1climres 25769 ellimc3 25934 lgsquadlem1 27442 lgsquadlem2 27443 wlkson 29692 0clwlk 30162 dmrab 32525 qusker 33342 bnj594 34888 satf0 35340 bj-elid6 37136 bj-imdirco 37156 wl-df4-3mintru2 37453 poimirlem4 37584 rabeqel 38210 iss2 38300 ifp1bi 43464 prprelprb 47391 prprspr2 47392 dfsclnbgr6 47730 eliunxp2 48058 |
Copyright terms: Public domain | W3C validator |