| 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 261 | . 2 ⊢ (𝜓 ↔ 𝜓) | |
| 2 | 1 | a1i 11 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: ifpbi23d 1080 3anbi12d 1439 3anbi13d 1440 3anbi23d 1441 3anbi1d 1442 3anbi2d 1443 3anbi3d 1444 nfald2 2450 exdistrf 2452 sb6x 2469 axc16gALT 2495 raleqOLD 3340 rexeqOLD 3341 vtoclegft 3588 ralxpxfr2d 3646 rr19.3v 3667 rr19.28v 3668 rabtru 3689 moeq3 3718 euxfr2w 3726 euxfr2 3728 reuxfrd 3754 dfif3 4540 sseliALT 5309 copsexgw 5495 copsexg 5496 soeq1 5613 frd 5641 soinxp 5767 idrefALT 6131 ordtri3or 6416 nfriotadw 7396 oprabidw 7462 ov6g 7597 ovg 7598 sorpssi 7749 dfxp3 8086 fsplit 8142 frxp3 8176 xpord3inddlem 8179 aceq1 10157 aceq2 10159 axpowndlem4 10640 axpownd 10641 ltsopr 11072 creur 12260 creui 12261 o1fsum 15849 sumodd 16425 sadfval 16489 sadcp1 16492 pceu 16884 vdwlem12 17030 sgrp2rid2ex 18940 gsumval3eu 19922 lss1d 20961 nrmr0reg 23757 stdbdxmet 24528 xrsxmet 24831 cmetcaulem 25322 bcth3 25365 iundisj2 25584 ulmdvlem3 26445 ulmdv 26446 dchrvmasumlem2 27542 colrot1 28567 lnrot1 28631 lnrot2 28632 wlkson 29674 trlsfval 29713 pthsfval 29739 spthsfval 29740 clwlks 29792 crcts 29808 cycls 29809 3cyclfrgrrn1 30304 frgrwopreg 30342 reuxfrdf 32510 iundisj2f 32603 iundisj2fi 32799 ordtprsuni 33918 pmeasmono 34326 erdszelem9 35204 satfv1fvfmla1 35428 opnrebl2 36322 wl-ifpimpr 37467 wl-df-3xor 37469 wl-ax11-lem9 37594 ax12fromc15 38906 axc16g-o 38935 ax12indalem 38946 ax12inda2ALT 38947 dihopelvalcpre 41250 lpolconN 41489 dvrelog2b 42067 isprimroot 42094 aks6d1c2p2 42120 hashscontpow 42123 rspcsbnea 42132 aks6d1c6lem3 42173 fsuppind 42600 zindbi 42958 cnvtrucl0 43637 ismnushort 44320 e2ebind 44583 uunT1 44800 ovnval2 46560 ovnval2b 46567 hoiqssbl 46640 6gbe 47758 8gbe 47760 isgrim 47868 usgrexmpl1tri 47984 gpgov 48001 gpg3kgrtriex 48045 |
| Copyright terms: Public domain | W3C validator |