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 229 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 |
This theorem is referenced by: pm5.5 365 a1bi 366 mtt 368 abai 825 dedlem0a 1039 ifptru 1071 norasslem2 1532 ceqsralt 3475 reu8 3672 csbiebt 3857 r19.3rz 4400 ralidm 4413 notzfausOLD 5228 reusv2lem5 5268 fncnv 6397 ovmpodxf 7279 brecop 8373 kmlem8 9568 kmlem13 9573 fin71num 9808 ttukeylem6 9925 ltxrlt 10700 rlimresb 14914 acsfn 16922 tgss2 21592 ist1-3 21954 mbflimsup 24270 mdegle0 24678 dchrelbas3 25822 tgcgr4 26325 wl-clabtv 34994 wl-clabt 34995 cdleme32fva 37733 ntrneik2 40795 ntrneix2 40796 ntrneikb 40797 ovmpordxf 44740 |
Copyright terms: Public domain | W3C validator |