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  4821  elrnmpt1  5007  fliftf  5971  elxp7  6363  eroveu  6859  sbthlemi5  7230  sbthlemi6  7231  elfi2  7258  sspw1or2  7494  reapltxor  8859  divap0b  8953  nnle1eq1  9257  nn0le0eq0  9520  nn0lt10b  9654  ioopos  10279  xrmaxiflemcom  11927  fz1f1o  12053  nndivdvds  12475  dvdsmultr2  12512  bitsmod  12635  pcmpt  13034  pcmpt2  13035  resrhm2b  14383  lssle0  14507  discld  14988  cncnpi  15080  cnptoprest2  15092  lmss  15098  txcn  15127  isxmet2d  15200  xblss2  15257  bdxmet  15353  xmetxp  15359  cncfcdm  15434  lgsneg  15884  lgsdilem  15887  2lgslem1a  15948  clwwlknonel  16414  clwwlknun  16423  eupth2lem2dc  16441