![]() |
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 | . 2 ⊢ 𝜑 | |
2 | ibar 521 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: mpbiran 696 cases 1023 truan 1518 2sb5rf 2416 euae 2686 rexv 3435 reuv 3436 rmov 3437 rabab 3438 euxfr 3622 euind 3623 dfdif3 3977 ddif 3999 nssinpss 4115 nsspssun 4116 vss 4272 reuprg0 4506 reuprg 4507 difsnpss 4608 sspr 4634 sstp 4635 disjprg 4919 mptv 5023 reusv2lem5 5150 oteqex2 5238 dfid4 5307 intirr 5812 xpcan 5867 fvopab6 6620 fnressn 6737 riotav 6936 mpov 7074 sorpss 7266 opabn1stprc 7557 fparlem2 7609 fnsuppres 7653 brtpos0 7695 sup0riota 8716 genpass 10221 nnwos 12122 hashbclem 13613 ccatlcan 13900 clim0 14714 gcd0id 15717 pjfval2 20545 mat1dimbas 20775 pmatcollpw2lem 21079 isbasis3g 21251 opnssneib 21417 ssidcn 21557 qtopcld 22015 mdegleb 24351 vieta1 24594 lgsne0 25603 axpasch 26420 0wlk 27635 0clwlk 27649 shlesb1i 28934 chnlei 29033 pjneli 29271 cvexchlem 29916 dmdbr5ati 29970 elimifd 30056 lmxrge0 30796 cntnevol 31089 bnj110 31738 elpotr 32486 dfbigcup2 32821 bj-rexvw 33629 bj-rababw 33630 finxpreclem4 34051 wl-cases2-dnf 34128 wl-euae 34133 wl-dfclab 34217 cnambfre 34329 triantru3 34892 lub0N 35718 glb0N 35722 cvlsupr3 35873 isdomn3 39145 ifpdfor2 39167 ifpdfor 39171 ifpim1 39175 ifpid2 39177 ifpim2 39178 ifpid2g 39200 ifpid1g 39201 ifpim23g 39202 ifpim1g 39208 ifpimimb 39211 rp-isfinite6 39225 rababg 39240 relnonrel 39254 rp-imass 39425 dffrege115 39632 funressnfv 42629 dfnelbr2 42824 |
Copyright terms: Public domain | W3C validator |