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  4798  elrnmpt1  4983  fliftf  5940  elxp7  6333  eroveu  6795  sbthlemi5  7160  sbthlemi6  7161  elfi2  7171  sspw1or2  7403  reapltxor  8769  divap0b  8863  nnle1eq1  9167  nn0le0eq0  9430  nn0lt10b  9560  ioopos  10185  xrmaxiflemcom  11811  fz1f1o  11937  nndivdvds  12359  dvdsmultr2  12396  bitsmod  12519  pcmpt  12918  pcmpt2  12919  resrhm2b  14266  lssle0  14389  discld  14863  cncnpi  14955  cnptoprest2  14967  lmss  14973  txcn  15002  isxmet2d  15075  xblss2  15132  bdxmet  15228  xmetxp  15234  cncfcdm  15309  lgsneg  15756  lgsdilem  15759  2lgslem1a  15820  clwwlknonel  16286  clwwlknun  16295  eupth2lem2dc  16313