![]() |
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 526 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ 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 197 df-an 385 |
This theorem is referenced by: mpbiran 991 cases 1029 truan 1648 2sb5rf 2586 rexv 3358 reuv 3359 rmov 3360 rabab 3361 euxfr 3531 euind 3532 dfdif3 3861 ddif 3883 nssinpss 3997 nsspssun 3998 vss 4153 difsnpss 4481 sspr 4509 sstp 4510 disjprg 4798 mptv 4901 reusv2lem5 5020 oteqex2 5109 dfid4 5174 intirr 5670 xpcan 5726 fvopab6 6471 fnressn 6586 riotav 6777 mpt2v 6913 sorpss 7105 opabn1stprc 7393 fparlem2 7444 fnsuppres 7489 brtpos0 7526 sup0riota 8534 genpass 10021 nnwos 11946 hashbclem 13426 ccatlcan 13670 clim0 14434 gcd0id 15440 pjfval2 20253 mat1dimbas 20478 pmatcollpw2lem 20782 isbasis3g 20953 opnssneib 21119 ssidcn 21259 qtopcld 21716 mdegleb 24021 vieta1 24264 lgsne0 25257 axpasch 26018 0wlk 27266 0clwlk 27280 shlesb1i 28552 chnlei 28651 pjneli 28889 cvexchlem 29534 dmdbr5ati 29588 elimifd 29667 lmxrge0 30305 cntnevol 30598 bnj110 31233 elpotr 31989 dfbigcup2 32310 bj-cleljustab 33151 bj-rexvwv 33170 bj-rababwv 33171 finxpreclem4 33540 wl-cases2-dnf 33606 cnambfre 33769 triantru3 34324 lub0N 34977 glb0N 34981 cvlsupr3 35132 isdomn3 38282 ifpdfor2 38305 ifpdfor 38309 ifpim1 38313 ifpid2 38315 ifpim2 38316 ifpid2g 38338 ifpid1g 38339 ifpim23g 38340 ifpim1g 38346 ifpimimb 38349 rp-isfinite6 38364 rababg 38379 relnonrel 38393 rp-imass 38565 dffrege115 38772 dfnelbr2 41797 |
Copyright terms: Public domain | W3C validator |