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  4676  elrnmpt1  4855  fliftf  5767  elxp7  6138  eroveu  6592  sbthlemi5  6926  sbthlemi6  6927  elfi2  6937  reapltxor  8487  divap0b  8579  nnle1eq1  8881  nn0le0eq0  9142  nn0lt10b  9271  ioopos  9886  xrmaxiflemcom  11190  fz1f1o  11316  nndivdvds  11736  dvdsmultr2  11773  pcmpt  12273  pcmpt2  12274  discld  12786  cncnpi  12878  cnptoprest2  12890  lmss  12896  txcn  12925  isxmet2d  12998  xblss2  13055  bdxmet  13151  xmetxp  13157  cncffvrn  13219  lgsneg  13575  lgsdilem  13578