![]() |
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 225 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 |
This theorem is referenced by: pm5.5 361 a1bi 362 mtt 364 abai 826 dedlem0a 1042 ifptru 1073 norasslem2 1529 ceqsralt 3504 clel2g 3645 clel4g 3650 reu8 3728 csbiebt 3922 r19.3rz 4497 ralidmOLD 4516 reusv2lem5 5402 fncnv 6626 ovmpodxf 7571 brecop 8829 kmlem8 10181 kmlem13 10186 fin71num 10421 ttukeylem6 10538 ltxrlt 11315 rlimresb 15542 acsfn 17639 tgss2 22903 ist1-3 23266 mbflimsup 25608 mdegle0 26026 dchrelbas3 27184 tgcgr4 28348 wl-clabtv 37064 wl-clabt 37065 cdleme32fva 39910 ntrneik2 43522 ntrneix2 43523 ntrneikb 43524 r19.3rzf 44529 ovmpordxf 47402 |
Copyright terms: Public domain | W3C validator |