![]() |
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 251 | . 2 ⊢ (𝜓 ↔ 𝜓) | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: 3anbi12d 1440 3anbi13d 1441 3anbi23d 1442 3anbi1d 1443 3anbi2d 1444 3anbi3d 1445 nfald2 2362 exdistrf 2364 ax12OLD 2372 axc16gALT 2395 sb6x 2412 ralxpxfr2d 3358 rr19.3v 3377 rr19.28v 3378 rabtru 3393 moeq3 3416 euxfr2 3424 dfif3 4133 sseliALT 4824 reuxfr2d 4921 copsexg 4985 soeq1 5083 soinxp 5217 ordtri3or 5793 ov6g 6840 ovg 6841 sorpssi 6985 dfxp3 7275 aceq1 8978 aceq2 8980 axpowndlem4 9460 axpownd 9461 ltsopr 9892 creur 11052 creui 11053 o1fsum 14589 sumodd 15158 sadfval 15221 sadcp1 15224 pceu 15598 vdwlem12 15743 sgrp2rid2ex 17461 gsumval3eu 18351 lss1d 19011 nrmr0reg 21600 stdbdxmet 22367 xrsxmet 22659 cmetcaulem 23132 bcth3 23174 iundisj2 23363 ulmdvlem3 24201 ulmdv 24202 dchrvmasumlem2 25232 colrot1 25499 lnrot1 25563 lnrot2 25564 dfcgra2 25766 isinag 25774 isrusgr 26513 wksfval 26561 wlkson 26608 trlsfval 26648 pthsfval 26673 spthsfval 26674 clwlks 26724 crcts 26739 cycls 26740 3cyclfrgrrn1 27265 frgrwopreg 27303 reuxfr3d 29456 iundisj2f 29529 iundisj2fi 29684 ordtprsuni 30093 isrnsigaOLD 30303 pmeasmono 30514 erdszelem9 31307 opnrebl2 32441 wl-ax11-lem9 33500 ax12fromc15 34509 axc16g-o 34538 ax12indalem 34549 ax12inda2ALT 34550 dihopelvalcpre 36854 lpolconN 37093 zindbi 37828 cnvtrucl0 38248 e2ebind 39096 uunT1 39324 trsbcVD 39427 ovnval2 41080 ovnval2b 41087 hoiqssbl 41160 6gbe 41984 8gbe 41986 |
Copyright terms: Public domain | W3C validator |