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  4694  elrnmpt1  4873  fliftf  5793  elxp7  6164  eroveu  6619  sbthlemi5  6953  sbthlemi6  6954  elfi2  6964  reapltxor  8523  divap0b  8616  nnle1eq1  8919  nn0le0eq0  9180  nn0lt10b  9309  ioopos  9924  xrmaxiflemcom  11228  fz1f1o  11354  nndivdvds  11774  dvdsmultr2  11811  pcmpt  12311  pcmpt2  12312  discld  13269  cncnpi  13361  cnptoprest2  13373  lmss  13379  txcn  13408  isxmet2d  13481  xblss2  13538  bdxmet  13634  xmetxp  13640  cncfcdm  13702  lgsneg  14058  lgsdilem  14061