Theorem biantrud 304

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

Syntax hints:   → wi 4   ∧ 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:  mpbiran2d  442  posng  4793  elrnmpt1  4978  fliftf  5932  elxp7  6325  eroveu  6786  sbthlemi5  7144  sbthlemi6  7145  elfi2  7155  reapltxor  8752  divap0b  8846  nnle1eq1  9150  nn0le0eq0  9413  nn0lt10b  9543  ioopos  10163  xrmaxiflemcom  11781  fz1f1o  11907  nndivdvds  12328  dvdsmultr2  12365  bitsmod  12488  pcmpt  12887  pcmpt2  12888  resrhm2b  14234  lssle0  14357  discld  14831  cncnpi  14923  cnptoprest2  14935  lmss  14941  txcn  14970  isxmet2d  15043  xblss2  15100  bdxmet  15196  xmetxp  15202  cncfcdm  15277  lgsneg  15724  lgsdilem  15727  2lgslem1a  15788