![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biimt | Structured version Visualization version GIF version |
Description: A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
biimt | ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . 2 ⊢ (𝜓 → (𝜑 → 𝜓)) | |
2 | pm2.27 42 | . 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 216 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: pm5.5 350 a1bi 351 mtt 353 abai 871 dedlem0a 1030 ifptru 1061 ceqsralt 3370 reu8 3544 csbiebt 3695 r19.3rz 4207 ralidm 4220 notzfaus 4990 reusv2lem5 5023 fncnv 6124 ovmpt2dxf 6953 brecop 8010 kmlem8 9192 kmlem13 9197 fin71num 9432 ttukeylem6 9549 ltxrlt 10321 rlimresb 14516 acsfn 16542 tgss2 21014 ist1-3 21376 mbflimsup 23653 mdegle0 24057 dchrelbas3 25184 tgcgr4 25647 cdleme32fva 36246 ntrneik2 38911 ntrneix2 38912 ntrneikb 38913 ovmpt2rdxf 42646 |
Copyright terms: Public domain | W3C validator |