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  4847  elrnmpt1  5033  fliftf  6005  elxp7  6404  eroveu  6900  sbthlemi5  7278  sbthlemi6  7279  elfi2  7306  sspw1or2  7544  reapltxor  8918  divap0b  9014  nnle1eq1  9329  nn0le0eq0  9593  nn0lt10b  9728  ioopos  10354  xrmaxiflemcom  12017  fz1f1o  12143  nndivdvds  12565  dvdsmultr2  12602  bitsmod  12725  pcmpt  13124  pcmpt2  13125  resrhm2b  14559  lssle0  14711  discld  15239  cncnpi  15331  cnptoprest2  15343  lmss  15349  txcn  15378  isxmet2d  15451  xblss2  15508  bdxmet  15604  xmetxp  15610  cncfcdm  15685  lgsneg  16155  lgsdilem  16158  2lgslem1a  16219  clwwlknonel  16685  clwwlknun  16694  eupth2lem2dc  16712