Theorem biantrurd 546

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

Hypothesis

Ref	Expression
biantrurd.1	|- (ph -> ps)

Assertion

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

Proof of Theorem biantrurd

Step	Hyp	Ref	Expression
1		biantrurd.1	. . 3 |- (ph -> ps)
2	1	biantrud 545	. 2 |- (ph -> (ch <-> (ch /\ ps)))
3		ancom 333	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
4	2, 3	syl6bb 414	1 |- (ph -> (ch <-> (ps /\ ch)))

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

This theorem is referenced by:  sbcgf 1469  reuxfr 1580  opbrop 2472  eloprabg 3035  mapxpen 3390  bnd2 3549  kmlem2 3581  iscard2 3660  nn2get 4438  elnnnn0 4594  ch0psst 5370  pjelt 5668  atcv0eq 5767

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