![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biantrur | Structured version Visualization version GIF 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 | . . 3 ⊢ 𝜑 | |
2 | 1 | biantru 529 | . 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
3 | 2 | biancomi 462 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 |
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 df-an 396 |
This theorem is referenced by: mpbiran 708 cases 1041 truan 1545 2sb5rf 2467 euae 2651 rexv 3496 reuv 3497 rmov 3498 rabab 3499 euxfrw 3715 euxfr 3717 euind 3718 dfdif3 4111 ddif 4133 nssinpss 4253 nsspssun 4254 notabw 4300 vss 4440 reuprg0 4703 reuprg 4704 difsnpss 4807 sspr 4833 sstp 4834 disjprgw 5138 disjprg 5139 mptv 5259 reusv2lem5 5397 oteqex2 5496 dfid4 5572 intirr 6119 xpcan 6175 resssxp 6269 fvopab6 7034 fnressn 7162 riotav 7376 mpov 7527 sorpss 7728 opabn1stprc 8057 fparlem2 8113 fnsuppres 8190 brtpos0 8233 naddrid 8698 sup0riota 9483 genpass 11027 nnwos 12924 hashbclem 14438 ccatlcan 14695 clim0 15477 gcd0id 16488 isdomn3 21242 pjfval2 21637 mat1dimbas 22368 pmatcollpw2lem 22673 isbasis3g 22846 opnssneib 23013 ssidcn 23153 qtopcld 23611 mdegleb 25994 vieta1 26241 lgsne0 27262 axpasch 28746 0wlk 29920 0clwlk 29934 shlesb1i 31190 chnlei 31289 pjneli 31527 cvexchlem 32172 dmdbr5ati 32226 elimifd 32328 lmxrge0 33548 cntnevol 33842 bnj110 34484 goeleq12bg 34954 fmlafvel 34990 elpotr 35372 dfbigcup2 35490 bj-rexvw 36353 bj-rababw 36354 bj-brab2a1 36623 finxpreclem4 36868 wl-cases2-dnf 36974 wl-euae 36979 wl-dfclab 37058 cnambfre 37136 triantru3 37694 lub0N 38656 glb0N 38660 cvlsupr3 38811 ifpdfor2 42882 ifpdfor 42886 ifpim1 42890 ifpid2 42892 ifpim2 42893 ifpid2g 42914 ifpid1g 42915 ifpim23g 42916 ifpim1g 42922 ifpimimb 42925 rp-isfinite6 42939 rababg 42995 relnonrel 43008 dffrege115 43399 funressnfv 46416 dfnelbr2 46644 |
Copyright terms: Public domain | W3C validator |