![]() |
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 453 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
3 | 1, 2 | bitr4i 270 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: anbi2ci 616 anbi1ci 617 anbi12ci 619 eu6lem 2593 elon2 6045 fununi 6267 fnopabg 6320 eqfnfv3 6635 respreima 6667 fsn 6726 brtpos2 7707 tpostpos 7721 oeeu 8036 mapval2 8242 xrltlen 12362 ssfzoulel 12952 xpcogend 14201 dfgcd2 15756 isffth2 17056 resscntz 18245 fiidomfld 19814 1stcelcls 21788 txflf 22333 fclsrest 22351 tsmssubm 22469 blres 22759 xrtgioo 23132 isncvsngp 23471 itg1climres 24033 ellimc3 24195 lgsquadlem1 25673 lgsquadlem2 25674 wlkson 27155 0clwlk 27674 dmrab 30054 qusker 30629 bnj594 31863 satf0 32222 rabeqel 35000 iss2 35087 prprelprb 43082 prprspr2 43083 eliunxp2 43781 |
Copyright terms: Public domain | W3C validator |