![]() |
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 8684 elpmg 8840 letri3 11304 mulsuble0b 12091 xrletri3 13138 qbtwnre 13183 iooneg 13453 invsym 17714 subsubc 17808 lsslss 20717 znleval 21330 restopn2 22902 elflim2 23689 ismet2 24060 mbfi1fseqlem4 25469 deg1ldg 25846 sincosq1sgn 26245 lgsquadlem3 27122 numclwwlkqhash 29896 rmounid 32003 dfrdg4 35228 bj-19.41t 35956 bj-0int 36286 orddif0suc 42321 dflim7 42326 naddsuc2 42446 mpbiran4d 47571 |
Copyright terms: Public domain | W3C validator |