Theorem biantru 543

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

Hypothesis

Ref	Expression
biantru.1	|- ph

Assertion

Ref	Expression
biantru	|- (ps <-> (ps /\ ph))

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 |- ph
2		iba 486	. 2 |- (ph -> (ps <-> (ps /\ ph)))
3	1, 2	ax-mp 6	1 |- (ps <-> (ps /\ ph))

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  mpbiranr 548  hbsb4t 906  isset 1351  eueq 1427  nsspssun 1666  disjpss 1738  pwun 1918  sucexb 2301  elvv 2464  resopab 2598  dfima2 2604  funfn 2689  fnfrn 2758  fnforn 2791  funforn 2792  f1orn 2809  fsn 2895  dfoprab2 3021  dom0 3367  mapdom2 3389  fiint 3445  cf0 3705  supsrlem5 4023  choc0 5291

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org