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  438  posng  4606  elrnmpt1  4785  fliftf  5693  elxp7  6061  eroveu  6513  sbthlemi5  6842  sbthlemi6  6843  elfi2  6853  reapltxor  8344  divap0b  8436  nnle1eq1  8737  nn0le0eq0  8998  nn0lt10b  9124  ioopos  9726  xrmaxiflemcom  11011  fz1f1o  11137  nndivdvds  11488  dvdsmultr2  11522  discld  12294  cncnpi  12386  cnptoprest2  12398  lmss  12404  txcn  12433  isxmet2d  12506  xblss2  12563  bdxmet  12659  xmetxp  12665  cncffvrn  12727