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 524 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: mpbiran 955 cases 1004 truan 1492 2sb5rf 2439 rexv 3193 reuv 3194 rmov 3195 rabab 3196 euxfr 3359 euind 3360 ddif 3704 nssinpss 3818 nsspssun 3819 vss 3964 difsnpss 4279 sspr 4306 sstp 4307 disjprg 4578 mptv 4679 reusv2lem5 4799 oteqex2 4888 dfid4 4955 intirr 5433 xpcan 5489 fvopab6 6218 fnressn 6330 riotav 6516 mpt2v 6648 sorpss 6840 fparlem2 7165 fnsuppres 7209 brtpos0 7246 sup0riota 8254 genpass 9710 nnwos 11631 hashbclem 13093 ccatlcan 13324 clim0 14085 gcd0id 15078 pjfval2 19872 mat1dimbas 20097 pmatcollpw2lem 20401 isbasis3g 20564 opnssneib 20729 ssidcn 20869 qtopcld 21326 mdegleb 23628 vieta1 23871 lgsne0 24860 axpasch 25621 0wlk 26075 0trl 26076 shlesb1i 27629 chnlei 27728 pjneli 27966 cvexchlem 28611 dmdbr5ati 28665 elimifd 28746 lmxrge0 29326 cntnevol 29618 bnj110 30182 elpotr 30930 nofulllem1 31101 dfbigcup2 31176 bj-rexvwv 32060 bj-rababwv 32061 bj-sspwpwab 32239 finxpreclem4 32407 wl-cases2-dnf 32474 cnambfre 32628 lub0N 33494 glb0N 33498 cvlsupr3 33649 isdomn3 36801 ifpdfor2 36824 ifpdfor 36828 ifpim1 36832 ifpid2 36834 ifpim2 36835 ifpid2g 36857 ifpid1g 36858 ifpim23g 36859 ifpim1g 36865 ifpimimb 36868 rp-isfinite6 36883 rababg 36898 relnonrel 36912 rp-imass 37085 dffrege115 37292 opabn1stprc 40318 01wlk 41284 |
Copyright terms: Public domain | W3C validator |