![]() |
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 1549 3anbi13d 1550 3anbi23d 1551 3anbi1d 1552 3anbi2d 1553 3anbi3d 1554 nfald2 2471 exdistrf 2473 ax12OLD 2481 axc16gALT 2504 sb6x 2521 ralxpxfr2d 3466 rr19.3v 3485 rr19.28v 3486 rabtru 3501 moeq3 3524 euxfr2 3532 dfif3 4244 sseliALT 4943 reuxfr2d 5040 copsexg 5104 soeq1 5206 soinxp 5340 ordtri3or 5916 ov6g 6964 ovg 6965 sorpssi 7109 dfxp3 7399 aceq1 9150 aceq2 9152 axpowndlem4 9634 axpownd 9635 ltsopr 10066 creur 11226 creui 11227 o1fsum 14764 sumodd 15333 sadfval 15396 sadcp1 15399 pceu 15773 vdwlem12 15918 sgrp2rid2ex 17635 gsumval3eu 18525 lss1d 19185 nrmr0reg 21774 stdbdxmet 22541 xrsxmet 22833 cmetcaulem 23306 bcth3 23348 iundisj2 23537 ulmdvlem3 24375 ulmdv 24376 dchrvmasumlem2 25407 colrot1 25674 lnrot1 25738 lnrot2 25739 dfcgra2 25941 isinag 25949 isrusgr 26688 wksfval 26736 wlkson 26783 trlsfval 26823 pthsfval 26848 spthsfval 26849 clwlks 26899 crcts 26915 cycls 26916 3cyclfrgrrn1 27460 frgrwopreg 27498 reuxfr3d 29658 iundisj2f 29731 iundisj2fi 29886 ordtprsuni 30295 isrnsigaOLD 30505 pmeasmono 30716 erdszelem9 31509 opnrebl2 32643 wl-ax11-lem9 33701 ax12fromc15 34712 axc16g-o 34741 ax12indalem 34752 ax12inda2ALT 34753 dihopelvalcpre 37057 lpolconN 37296 zindbi 38031 cnvtrucl0 38451 e2ebind 39299 uunT1 39527 trsbcVD 39630 ovnval2 41283 ovnval2b 41290 hoiqssbl 41363 6gbe 42187 8gbe 42189 |
Copyright terms: Public domain | W3C validator |