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 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbiran2d  446  posng  4849  elrnmpt1  5035  fliftf  6008  elxp7  6408  eroveu  6904  sbthlemi5  7284  sbthlemi6  7285  elfi2  7312  sspw1or2  7551  reapltxor  8926  divap0b  9022  nnle1eq1  9338  nn0le0eq0  9603  nn0lt10b  9738  ioopos  10370  xrmaxiflemcom  12041  fz1f1o  12167  nndivdvds  12589  dvdsmultr2  12626  bitsmod  12749  pcmpt  13152  pcmpt2  13153  resrhm2b  14667  lssle0  14819  discld  15374  cncnpi  15466  cnptoprest2  15478  lmss  15484  txcn  15513  isxmet2d  15586  xblss2  15643  bdxmet  15739  xmetxp  15745  cncfcdm  15820  lgsneg  16360  lgsdilem  16363  2lgslem1a  16424  clwwlknonel  16890  clwwlknun  16899  eupth2lem2dc  16917