![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biantrur | Structured version Visualization version Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
biantrur.1 |
![]() ![]() |
Ref | Expression |
---|---|
biantrur |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrur.1 |
. 2
![]() ![]() | |
2 | ibar 507 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-an 373 |
This theorem is referenced by: mpbiran 929 cases 982 truan 1461 2sb5rf 2280 rexv 3062 reuv 3063 rmov 3064 rabab 3065 euxfr 3224 euind 3225 ddif 3565 nssinpss 3675 nsspssun 3676 vss 3801 difsnpss 4115 sspr 4135 sstp 4136 disjprg 4398 mptv 4496 reusv2lem5 4608 oteqex2 4693 dfid4 4751 intirr 5218 xpcan 5273 fvopab6 5975 fnressn 6076 riotav 6257 mpt2v 6386 sorpss 6576 fparlem2 6897 fnsuppres 6942 brtpos0 6980 sup0riota 7979 genpass 9434 nnwos 11226 hashbclem 12615 ccatlcan 12828 clim0 13570 gcd0id 14487 pjfval2 19272 mat1dimbas 19497 pmatcollpw2lem 19801 isbasis3g 19964 opnssneib 20131 ssidcn 20271 qtopcld 20728 mdegleb 23013 vieta1 23265 lgsne0 24261 axpasch 24971 0wlk 25275 0trl 25276 shlesb1i 27039 chnlei 27138 pjneli 27376 cvexchlem 28021 dmdbr5ati 28075 elimifd 28160 lmxrge0 28758 cntnevol 29050 bnj110 29669 elpotr 30427 nofulllem1 30591 dfbigcup2 30666 bj-rexvwv 31475 bj-rababwv 31476 finxpreclem4 31786 wl-cases2-dnf 31850 cnambfre 31989 lub0N 32755 glb0N 32759 cvlsupr3 32910 isdomn3 36081 ifpdfor2 36104 ifpdfor 36108 ifpim1 36112 ifpid2 36114 ifpim2 36115 ifpid2g 36137 ifpid1g 36138 ifpim23g 36139 ifpim1g 36145 ifpimimb 36148 rp-isfinite6 36163 rababg 36179 relnonrel 36193 rp-imass 36366 dffrege115 36574 opabn1stprc 39007 01wlk 39704 |
Copyright terms: Public domain | W3C validator |