Theorem biantrud 300

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 296	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran2d  436  posng  4571  elrnmpt1  4750  fliftf  5654  elxp7  6022  eroveu  6474  sbthlemi5  6801  sbthlemi6  6802  elfi2  6812  reapltxor  8269  divap0b  8356  nnle1eq1  8654  nn0le0eq0  8909  nn0lt10b  9035  ioopos  9626  xrmaxiflemcom  10910  fz1f1o  11036  nndivdvds  11347  dvdsmultr2  11381  discld  12148  cncnpi  12239  cnptoprest2  12251  lmss  12257  txcn  12286  isxmet2d  12337  xblss2  12394  bdxmet  12490  xmetxp  12496  cncffvrn  12555