![]() |
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 260 | . 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 1077 3anbi12d 1433 3anbi13d 1434 3anbi23d 1435 3anbi1d 1436 3anbi2d 1437 3anbi3d 1438 nfald2 2438 exdistrf 2440 sb6x 2457 axc16gALT 2483 raleqOLD 3324 rexeqOLD 3325 vtoclegft 3568 ralxpxfr2d 3629 rr19.3v 3652 rr19.28v 3653 rabtru 3676 moeq3 3704 euxfr2w 3712 euxfr2 3714 reuxfrd 3740 dfif3 4544 sseliALT 5310 copsexgw 5492 copsexg 5493 soeq1 5611 frd 5637 soinxp 5759 idrefALT 6118 ordtri3or 6403 nfriotadw 7383 oprabidw 7450 ov6g 7585 ovg 7586 sorpssi 7735 dfxp3 8066 fsplit 8122 frxp3 8156 xpord3inddlem 8159 aceq1 10142 aceq2 10144 axpowndlem4 10625 axpownd 10626 ltsopr 11057 creur 12239 creui 12240 o1fsum 15795 sumodd 16368 sadfval 16430 sadcp1 16433 pceu 16818 vdwlem12 16964 sgrp2rid2ex 18887 gsumval3eu 19871 lss1d 20859 nrmr0reg 23697 stdbdxmet 24468 xrsxmet 24769 cmetcaulem 25260 bcth3 25303 iundisj2 25522 ulmdvlem3 26383 ulmdv 26384 dchrvmasumlem2 27476 colrot1 28435 lnrot1 28499 lnrot2 28500 wlkson 29542 trlsfval 29581 pthsfval 29607 spthsfval 29608 clwlks 29658 crcts 29674 cycls 29675 3cyclfrgrrn1 30167 frgrwopreg 30205 reuxfrdf 32367 iundisj2f 32459 iundisj2fi 32647 ordtprsuni 33648 pmeasmono 34072 erdszelem9 34937 satfv1fvfmla1 35161 opnrebl2 35933 wl-ifpimpr 37073 wl-df-3xor 37075 wl-ax11-lem9 37188 ax12fromc15 38504 axc16g-o 38533 ax12indalem 38544 ax12inda2ALT 38545 dihopelvalcpre 40848 lpolconN 41087 dvrelog2b 41666 isprimroot 41693 aks6d1c2p2 41719 hashscontpow 41722 rspcsbnea 41731 sticksstones11 41756 aks6d1c6lem3 41772 fsuppind 41955 zindbi 42506 cnvtrucl0 43193 ismnushort 43877 e2ebind 44141 uunT1 44358 ovnval2 46068 ovnval2b 46075 hoiqssbl 46148 6gbe 47245 8gbe 47247 isgrim 47349 |
Copyright terms: Public domain | W3C validator |