![]() |
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 2570 elon2 6405 fununi 6652 fnopabg 6716 eqfnfv3 7064 respreima 7097 fsn 7167 brtpos2 8269 tpostpos 8283 oeeu 8655 mapval2 8926 xrltlen 13204 ssfzoulel 13806 xpcogend 15019 dfgcd2 16587 isffth2 17978 resscntz 19368 fiidomfld 20792 1stcelcls 23483 txflf 24028 fclsrest 24046 tsmssubm 24165 blres 24455 xrtgioo 24840 isncvsngp 25195 itg1climres 25762 ellimc3 25926 lgsquadlem1 27433 lgsquadlem2 27434 wlkson 29683 0clwlk 30153 dmrab 32516 qusker 33334 bnj594 34880 satf0 35332 bj-elid6 37084 bj-imdirco 37104 wl-df4-3mintru2 37401 poimirlem4 37532 rabeqel 38158 iss2 38248 ifp1bi 43404 prprelprb 47323 prprspr2 47324 dfsclnbgr6 47659 eliunxp2 47976 |
Copyright terms: Public domain | W3C validator |