Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpbirand | Structured version Visualization version GIF version |
Description: Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Ref | Expression |
---|---|
mpbirand.1 | ⊢ (𝜑 → 𝜒) |
mpbirand.2 | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Ref | Expression |
---|---|
mpbirand | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbirand.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | |
2 | mpbirand.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 2 | biantrurd 536 | . 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃))) |
4 | 1, 3 | bitr4d 285 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: mpbiran2d 708 3anibar 1331 rmob2 3804 opbrop 5645 wemapso2lem 9168 uzin 12474 supxrre1 12920 ixxun 12951 uzsplit 13184 pfxsuffeqwrdeq 14263 ello12 15077 elo12 15088 fsumss 15289 fprodss 15510 ramval 16561 issect2 17259 lspsnel5 20032 cnprest 22186 cnprest2 22187 cnt0 22243 1stccn 22360 kgencn 22453 qtopcn 22611 fbflim 22873 isflf 22890 cnflf 22899 fclscf 22922 cnfcf 22939 elbl2ps 23287 elbl2 23288 metcn 23441 txmetcn 23446 iscvs 24024 lmclimf 24201 ovolfioo 24364 ovolficc 24365 ovoliun 24402 ismbl2 24424 mbfmulc2lem 24544 mbfmax 24546 mbfposr 24549 mbfaddlem 24557 mbfsup 24561 mbfi1fseqlem4 24616 itg2monolem1 24648 itg2cnlem1 24659 tgellng 26644 isleag 26938 ttgelitv 26974 isspthonpth 27836 clwlkclwwlkflem 28087 clwwlkwwlksb 28137 fvdifsupp 30738 lindflbs 31288 ismntoplly 31687 esum2dlem 31772 ntrclselnel1 41344 ntrneicls00 41376 vonvolmbl 43874 dfdfat2 44292 ipolubdm 45946 ipoglbdm 45949 functhinc 45999 |
Copyright terms: Public domain | W3C validator |