![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rbaib | Structured version Visualization version GIF version |
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
Ref | Expression |
---|---|
baib.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
rbaib | ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | baib.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | rbaibr 539 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
3 | 2 | bicomd 222 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 398 |
This theorem is referenced by: pm5.75 1028 cador 1610 reusv1 5356 reusv2lem1 5357 fpwwe2 10587 fzsplit2 13475 saddisjlem 16352 smupval 16376 smueqlem 16378 prmrec 16802 ablnsg 19633 cnprest 22663 flimrest 23357 fclsrest 23398 tsmssubm 23517 setsxms 23857 tcphcph 24624 ellimc2 25264 fsumvma2 26585 chpub 26591 mdbr2 31287 mdsl2i 31313 fzsplit3 31751 posrasymb 31881 trleile 31887 fvineqsneu 35932 cnvcnvintabd 41964 grumnud 42658 mofeu 47004 |
Copyright terms: Public domain | W3C validator |