![]() |
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 205 |
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 206 |
This theorem is referenced by: ifpbi23d 1081 3anbi12d 1438 3anbi13d 1439 3anbi23d 1440 3anbi1d 1441 3anbi2d 1442 3anbi3d 1443 nfald2 2444 exdistrf 2446 sb6x 2463 axc16gALT 2489 raleq 3308 rexeq 3309 vtoclegft 3541 ralxpxfr2d 3597 rr19.3v 3620 rr19.28v 3621 rabtru 3643 moeq3 3671 euxfr2w 3679 euxfr2 3681 reuxfrd 3707 dfif3 4501 sseliALT 5267 copsexgw 5448 copsexg 5449 soeq1 5567 frd 5593 soinxp 5714 idrefALT 6066 ordtri3or 6350 nfriotadw 7322 oprabidw 7389 ov6g 7519 ovg 7520 sorpssi 7667 dfxp3 7994 fsplit 8050 frxp3 8084 xpord3inddlem 8087 aceq1 10058 aceq2 10060 axpowndlem4 10541 axpownd 10542 ltsopr 10973 creur 12152 creui 12153 o1fsum 15703 sumodd 16275 sadfval 16337 sadcp1 16340 pceu 16723 vdwlem12 16869 sgrp2rid2ex 18742 gsumval3eu 19686 lss1d 20439 nrmr0reg 23116 stdbdxmet 23887 xrsxmet 24188 cmetcaulem 24668 bcth3 24711 iundisj2 24929 ulmdvlem3 25777 ulmdv 25778 dchrvmasumlem2 26862 colrot1 27543 lnrot1 27607 lnrot2 27608 wlkson 28646 trlsfval 28685 pthsfval 28711 spthsfval 28712 clwlks 28762 crcts 28778 cycls 28779 3cyclfrgrrn1 29271 frgrwopreg 29309 reuxfrdf 31462 iundisj2f 31554 iundisj2fi 31747 ordtprsuni 32557 pmeasmono 32981 erdszelem9 33850 satfv1fvfmla1 34074 opnrebl2 34839 wl-ifpimpr 35983 wl-df-3xor 35985 wl-ax11-lem9 36091 ax12fromc15 37413 axc16g-o 37442 ax12indalem 37453 ax12inda2ALT 37454 dihopelvalcpre 39757 lpolconN 39996 dvrelog2b 40569 aks6d1c2p2 40595 sticksstones11 40610 fsuppind 40808 zindbi 41313 cnvtrucl0 41984 ismnushort 42669 e2ebind 42933 uunT1 43150 ovnval2 44872 ovnval2b 44879 hoiqssbl 44952 6gbe 46049 8gbe 46051 |
Copyright terms: Public domain | W3C validator |