![]() |
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 707 naddcom 8696 elpmg 8853 letri3 11321 mulsuble0b 12108 xrletri3 13157 qbtwnre 13202 iooneg 13472 invsym 17736 subsubc 17830 lsslss 20834 znleval 21475 restopn2 23068 elflim2 23855 ismet2 24226 mbfi1fseqlem4 25635 deg1ldg 26015 sincosq1sgn 26420 lgsquadlem3 27302 renegscl 28213 numclwwlkqhash 30172 rmounid 32279 dfrdg4 35483 bj-19.41t 36187 bj-0int 36516 orddif0suc 42620 dflim7 42625 naddsuc2 42745 mpbiran4d 47793 |
Copyright terms: Public domain | W3C validator |