|   | 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 206 ∧ 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 207 df-an 396 | 
| This theorem is referenced by: mpbiran 709 cases 1042 truan 1550 2sb5rf 2476 euae 2659 rexv 3508 reuv 3509 rmov 3510 rabab 3511 euxfrw 3726 euxfr 3728 euind 3729 dfdif3OLD 4117 ddif 4140 nssinpss 4266 nsspssun 4267 notabw 4312 vss 4445 reuprg0 4701 reuprg 4702 difsnpss 4806 sspr 4834 sstp 4835 disjprg 5138 mptv 5257 reusv2lem5 5401 oteqex2 5503 dfid4 5578 intirr 6137 xpcan 6195 resssxp 6289 fvopab6 7049 fnressn 7177 riotav 7394 mpov 7546 sorpss 7749 opabn1stprc 8084 fparlem2 8139 fnsuppres 8217 brtpos0 8259 naddrid 8722 sup0riota 9506 genpass 11050 nnwos 12958 hashbclem 14492 ccatlcan 14757 clim0 15543 gcd0id 16557 isdomn3 20716 pjfval2 21730 mat1dimbas 22479 pmatcollpw2lem 22784 isbasis3g 22957 opnssneib 23124 ssidcn 23264 qtopcld 23722 mdegleb 26104 vieta1 26355 lgsne0 27380 axpasch 28957 0wlk 30136 0clwlk 30150 shlesb1i 31406 chnlei 31505 pjneli 31743 cvexchlem 32388 dmdbr5ati 32442 elimifd 32557 fzo0opth 32808 1arithidom 33566 lmxrge0 33952 cntnevol 34230 bnj110 34873 goeleq12bg 35355 fmlafvel 35391 elpotr 35783 dfbigcup2 35901 bj-rexvw 36882 bj-rababw 36883 bj-brab2a1 37151 finxpreclem4 37396 wl-cases2-dnf 37514 wl-euae 37519 wl-dfclab 37598 cnambfre 37676 triantru3 38232 lub0N 39191 glb0N 39195 cvlsupr3 39346 ifpdfor2 43479 ifpdfor 43483 ifpim1 43487 ifpid2 43489 ifpim2 43490 ifpid2g 43511 ifpid1g 43512 ifpim23g 43513 ifpim1g 43519 ifpimimb 43522 rp-isfinite6 43536 rababg 43592 relnonrel 43605 dffrege115 43996 funressnfv 47060 dfnelbr2 47290 edgusgrclnbfin 47833 | 
| Copyright terms: Public domain | W3C validator |