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  950  isset  2822  rexcom4b  2841  eueq  2990  ssrabeq  3328  a9evsep  4234  pwunim  4409  elvv  4814  elvvv  4815  resopab  5084  funfn  5384  dffn2  5512  dffn3  5521  dffn4  5598  fsn  5851  ixp0x  6963  ac6sfi  7157  fimax2gtri  7161  nninfwlporlemd  7465  ccatrcan  11419  xrmaxiflemcom  11942  plyun0  15650  trirec0xor  16878