![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biidd | Structured version Visualization version GIF version |
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
Ref | Expression |
---|---|
biidd | ⊢ (𝜑 → (𝜓 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 253 | . 2 ⊢ (𝜓 ↔ 𝜓) | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: 3anbi12d 1416 3anbi13d 1417 3anbi23d 1418 3anbi1d 1419 3anbi2d 1420 3anbi3d 1421 nfald2 2381 exdistrf 2383 sb6x 2402 axc16gALT 2450 raleq 3346 rexeq 3347 ralxpxfr2d 3555 rr19.3v 3576 rr19.28v 3577 rabtru 3593 moeq3 3618 euxfr2 3626 reuxfr3d 3652 dfif3 4364 sseliALT 5070 copsexg 5238 soeq1 5346 soinxp 5483 idrefALT 5813 ordtri3or 6061 ov6g 7128 ovg 7129 sorpssi 7273 dfxp3 7567 aceq1 9337 aceq2 9339 axpowndlem4 9820 axpownd 9821 ltsopr 10252 creur 11433 creui 11434 o1fsum 15028 sumodd 15599 sadfval 15661 sadcp1 15664 pceu 16039 vdwlem12 16184 sgrp2rid2ex 17883 gsumval3eu 18778 lss1d 19457 nrmr0reg 22061 stdbdxmet 22828 xrsxmet 23120 cmetcaulem 23594 bcth3 23637 iundisj2 23853 ulmdvlem3 24693 ulmdv 24694 dchrvmasumlem2 25776 colrot1 26047 lnrot1 26111 lnrot2 26112 wksfval 27094 wlkson 27140 trlsfval 27183 pthsfval 27210 spthsfval 27211 clwlks 27261 crcts 27277 cycls 27278 3cyclfrgrrn1 27819 frgrwopreg 27857 iundisj2f 30106 iundisj2fi 30269 ordtprsuni 30803 isrnsigaOLD 31013 pmeasmono 31224 erdszelem9 32028 opnrebl2 33187 wl-ax11-lem9 34263 ax12fromc15 35483 axc16g-o 35512 ax12indalem 35523 ax12inda2ALT 35524 dihopelvalcpre 37826 lpolconN 38065 zindbi 38936 cnvtrucl0 39344 e2ebind 40313 uunT1 40530 ovnval2 42256 ovnval2b 42263 hoiqssbl 42336 6gbe 43302 8gbe 43304 |
Copyright terms: Public domain | W3C validator |