Theorem biantru 302

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)

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 300	. 2 |- ( ph -> ( ps <-> ( ps /\ ph ) ) )
3	1, 2	ax-mp 5	1 |- ( ps <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.71  389  mpbiran2  946  isset  2786  rexcom4b  2805  eueq  2954  ssrabeq  3291  a9evsep  4185  pwunim  4354  elvv  4758  elvvv  4759  resopab  5025  funfn  5324  dffn2  5451  dffn3  5460  dffn4  5530  fsn  5780  ixp0x  6843  ac6sfi  7028  fimax2gtri  7031  nninfwlporlemd  7307  ccatrcan  11217  xrmaxiflemcom  11726  plyun0  15375  trirec0xor  16324