| 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 532 | . 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃))) |
| 4 | 1, 3 | bitr4d 282 | 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: mpbiran2d 708 3anibar 1330 rmob2 3892 opbrop 5783 fvdifsupp 8196 wemapso2lem 9592 uzin 12918 supxrre1 13372 ixxun 13403 uzsplit 13636 pfxsuffeqwrdeq 14736 ello12 15552 elo12 15563 fsumss 15761 fprodss 15984 ramval 17046 issect2 17798 ellspsn5b 20993 cnprest 23297 cnprest2 23298 cnt0 23354 1stccn 23471 kgencn 23564 qtopcn 23722 fbflim 23984 isflf 24001 cnflf 24010 fclscf 24033 cnfcf 24050 elbl2ps 24399 elbl2 24400 metcn 24556 txmetcn 24561 iscvs 25160 lmclimf 25338 ovolfioo 25502 ovolficc 25503 ovoliun 25540 ismbl2 25562 mbfmulc2lem 25682 mbfmax 25684 mbfposr 25687 mbfaddlem 25695 mbfsup 25699 mbfi1fseqlem4 25753 itg2monolem1 25785 itg2cnlem1 25796 tgellng 28561 isleag 28855 ttgelitv 28897 isspthonpth 29769 clwlkclwwlkflem 30023 clwwlkwwlksb 30073 lindflbs 33407 ply1degleel 33616 algextdeglem7 33764 ismntoplly 34026 esum2dlem 34093 ntrclselnel1 44070 ntrneicls00 44102 vonvolmbl 46676 dfdfat2 47140 ipolubdm 48876 ipoglbdm 48879 isup 48937 functhinc 49097 |
| Copyright terms: Public domain | W3C validator |