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 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.71  393  mpbiran2  954  isset  2828  rexcom4b  2847  eueq  2997  ssrabeq  3336  a9evsep  4257  pwunim  4433  elvv  4839  elvvv  4840  resopab  5110  funfn  5410  dffn2  5538  dffn3  5547  dffn4  5624  fsn  5883  ixp0x  7014  ac6sfi  7208  fimax2gtri  7212  nninfwlporlemd  7518  ccatrcan  11512  xrmaxiflemcom  12039  plyun0  15979  trirec0xor  17318