Theorem biantrud 302

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

Hypothesis

Ref	Expression
biantrud.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
biantrud	⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 ⊢ (𝜑 → 𝜓)
2		iba 298	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ 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:  mpbiran2d  439  posng  4670  elrnmpt1  4849  fliftf  5761  elxp7  6130  eroveu  6583  sbthlemi5  6917  sbthlemi6  6918  elfi2  6928  reapltxor  8478  divap0b  8570  nnle1eq1  8872  nn0le0eq0  9133  nn0lt10b  9262  ioopos  9877  xrmaxiflemcom  11176  fz1f1o  11302  nndivdvds  11722  dvdsmultr2  11758  pcmpt  12250  pcmpt2  12251  discld  12677  cncnpi  12769  cnptoprest2  12781  lmss  12787  txcn  12816  isxmet2d  12889  xblss2  12946  bdxmet  13042  xmetxp  13048  cncffvrn  13110