![]() |
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 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: ibar 528 rbaibd 540 pm4.71rd 562 anbi1cd 635 mpbiran2d 708 naddcom 8719 naddsuc2 8738 elpmg 8882 letri3 11344 mulsuble0b 12138 xrletri3 13193 qbtwnre 13238 iooneg 13508 invsym 17810 subsubc 17904 lsslss 20977 znleval 21591 restopn2 23201 elflim2 23988 ismet2 24359 mbfi1fseqlem4 25768 deg1ldg 26146 sincosq1sgn 26555 lgsquadlem3 27441 renegscl 28445 numclwwlkqhash 30404 rmounid 32523 dfrdg4 35933 bj-19.41t 36757 bj-0int 37084 orddif0suc 43258 dflim7 43263 mpbiran4d 48647 |
Copyright terms: Public domain | W3C validator |