Theorem biantru 300

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.71  387  mpbiran2  926  isset  2718  rexcom4b  2737  eueq  2883  ssrabeq  3214  a9evsep  4086  pwunim  4246  elvv  4648  elvvv  4649  resopab  4910  funfn  5200  dffn2  5321  dffn3  5330  dffn4  5398  fsn  5639  ixp0x  6671  ac6sfi  6843  fimax2gtri  6846  xrmaxiflemcom  11146  trirec0xor  13616