![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biancomd | Structured version Visualization version GIF version |
Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.) |
Ref | Expression |
---|---|
biancomd.1 | ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒))) |
Ref | Expression |
---|---|
biancomd | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biancomd.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒))) | |
2 | ancom 460 | . 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃)) | |
3 | 1, 2 | bitrdi 287 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: ibar 528 rbaibd 540 pm4.71rd 562 anbi1cd 633 mpbiran2d 705 naddcom 8687 elpmg 8843 letri3 11306 mulsuble0b 12093 xrletri3 13140 qbtwnre 13185 iooneg 13455 invsym 17716 subsubc 17810 lsslss 20720 znleval 21333 restopn2 22914 elflim2 23701 ismet2 24072 mbfi1fseqlem4 25481 deg1ldg 25859 sincosq1sgn 26259 lgsquadlem3 27136 numclwwlkqhash 29910 rmounid 32017 dfrdg4 35242 bj-19.41t 35968 bj-0int 36298 orddif0suc 42333 dflim7 42338 naddsuc2 42458 mpbiran4d 47583 |
Copyright terms: Public domain | W3C validator |