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 41 | . 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 215 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: pm5.5 350 a1bi 351 mtt 353 abai 832 dedlem0a 991 ifptru 1017 ceqsralt 3202 reu8 3369 csbiebt 3519 r19.3rz 4014 ralidm 4027 notzfaus 4766 reusv2lem5 4799 fncnv 5876 ovmpt2dxf 6684 brecop 7727 kmlem8 8862 kmlem13 8867 fin71num 9102 ttukeylem6 9219 ltxrlt 9987 rlimresb 14144 acsfn 16143 tgss2 20602 ist1-3 20963 mbflimsup 23239 mdegle0 23641 dchrelbas3 24763 tgcgr4 25226 cdleme32fva 34743 ntrneik2 37410 ntrneix2 37411 ntrneikb 37412 ovmpt2rdxf 41910 |
Copyright terms: Public domain | W3C validator |