Theorem biantru 302

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

Hypothesis

Ref	Expression
biantru.1	⊢ 𝜑

Assertion

Ref	Expression
biantru	⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 ⊢ 𝜑
2		iba 300	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

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  393  mpbiran2  954  isset  2828  rexcom4b  2847  eueq  2997  ssrabeq  3336  a9evsep  4253  pwunim  4429  elvv  4835  elvvv  4836  resopab  5105  funfn  5405  dffn2  5533  dffn3  5542  dffn4  5619  fsn  5874  ixp0x  7001  ac6sfi  7195  fimax2gtri  7199  nninfwlporlemd  7505  ccatrcan  11472  xrmaxiflemcom  11996  plyun0  15763  trirec0xor  17002