| 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 226 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 |
| This theorem is referenced by: pm5.5 361 a1bi 362 mtt 364 abai 827 dedlem0a 1044 ifptru 1075 norasslem2 1535 ceqsralt 3516 clel2g 3659 clel4g 3663 reu8 3739 csbiebt 3928 r19.3rz 4497 reusv2lem5 5402 fncnv 6639 ovmpodxf 7583 brecop 8850 kmlem8 10198 kmlem13 10203 fin71num 10437 ttukeylem6 10554 ltxrlt 11331 rlimresb 15601 acsfn 17702 tgss2 22994 ist1-3 23357 mbflimsup 25701 mdegle0 26116 dchrelbas3 27282 tgcgr4 28539 wl-clabtv 37598 wl-clabt 37599 cdleme32fva 40439 ntrneik2 44105 ntrneix2 44106 ntrneikb 44107 r19.3rzf 45163 ovmpordxf 48255 fulltermc 49143 |
| Copyright terms: Public domain | W3C validator |