![]() |
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 461 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
3 | 1, 2 | bitr4i 277 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: biantrur 531 rbaibr 538 pm4.71ri 561 anbi2ci 625 anbi1ci 626 anbi12ci 628 an12 643 an32 644 mpbiran2 708 eu6lem 2567 elon2 6372 fununi 6620 fnopabg 6684 eqfnfv3 7031 respreima 7064 fsn 7129 brtpos2 8213 tpostpos 8227 oeeu 8599 mapval2 8862 xrltlen 13121 ssfzoulel 13722 xpcogend 14917 dfgcd2 16484 isffth2 17863 resscntz 19191 fiidomfld 20919 1stcelcls 22956 txflf 23501 fclsrest 23519 tsmssubm 23638 blres 23928 xrtgioo 24313 isncvsngp 24657 itg1climres 25223 ellimc3 25387 lgsquadlem1 26872 lgsquadlem2 26873 wlkson 28902 0clwlk 29372 dmrab 31724 qusker 32452 bnj594 33911 satf0 34351 bj-elid6 36039 bj-imdirco 36059 wl-df4-3mintru2 36356 poimirlem4 36480 rabeqel 37110 iss2 37201 ifp1bi 42238 prprelprb 46171 prprspr2 46172 eliunxp2 46962 |
Copyright terms: Public domain | W3C validator |