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  4796  elrnmpt1  4981  fliftf  5935  elxp7  6328  eroveu  6790  sbthlemi5  7154  sbthlemi6  7155  elfi2  7165  reapltxor  8762  divap0b  8856  nnle1eq1  9160  nn0le0eq0  9423  nn0lt10b  9553  ioopos  10178  xrmaxiflemcom  11803  fz1f1o  11929  nndivdvds  12350  dvdsmultr2  12387  bitsmod  12510  pcmpt  12909  pcmpt2  12910  resrhm2b  14256  lssle0  14379  discld  14853  cncnpi  14945  cnptoprest2  14957  lmss  14963  txcn  14992  isxmet2d  15065  xblss2  15122  bdxmet  15218  xmetxp  15224  cncfcdm  15299  lgsneg  15746  lgsdilem  15749  2lgslem1a  15810  clwwlknonel  16241  clwwlknun  16250