biantru - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem biantru 722

Description: A wff is equivalent to its conjunction with truth.

**Hypothesis**
Ref	Expression
biantru.1

**Assertion**
Ref	Expression
biantru	$/\$

**Proof of Theorem biantru**
Step	Hyp	Ref	Expression
1		biantru.1	. 2
2		iba 640	. 2 $/\$
3	1, 2	ax-mp 7	1 $/\$

Colors of variables: wff set class

Syntax hints:

wb 146 $/\$ wa 223

This theorem is referenced by: mpbiran2 727 hbsb4t 1244 isset 1805 eueq 1907 nsspssun 2231 disjpss 2309 pwundif 2817 pwun 2818 dfid3 2826 sucexb 3038 elvv 3218 resopab 3379 dfima2 3389 xp11a 3464 funfn 3528 fnfrn 3619 fnforn 3662 f1orn 3683 fsn 3819 dfoprab2 3976 ixp0x 4343 dom0 4445 mapdom2 4474 fiint 4534 rankc1 4677 cf0 4882 supsrlem5 5201 eltopsp 7546 islp2 7688 nmolb 8366 choc0 9205 nmoplbt 9748 nmfnlbt 9764 dmdbr5at 10255 symgval 10308 symggrpiOLD 10311 symggrpi 10313

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7

This theorem depends on definitions: df-bi 147 df-an 225