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  941  isset  2744  rexcom4b  2763  eueq  2909  ssrabeq  3243  a9evsep  4126  pwunim  4287  elvv  4689  elvvv  4690  resopab  4952  funfn  5247  dffn2  5368  dffn3  5377  dffn4  5445  fsn  5689  ixp0x  6726  ac6sfi  6898  fimax2gtri  6901  nninfwlporlemd  7170  xrmaxiflemcom  11257  trirec0xor  14796