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  4800  elrnmpt1  4985  fliftf  5945  elxp7  6338  eroveu  6800  sbthlemi5  7165  sbthlemi6  7166  elfi2  7176  sspw1or2  7408  reapltxor  8774  divap0b  8868  nnle1eq1  9172  nn0le0eq0  9435  nn0lt10b  9565  ioopos  10190  xrmaxiflemcom  11832  fz1f1o  11958  nndivdvds  12380  dvdsmultr2  12417  bitsmod  12540  pcmpt  12939  pcmpt2  12940  resrhm2b  14287  lssle0  14410  discld  14889  cncnpi  14981  cnptoprest2  14993  lmss  14999  txcn  15028  isxmet2d  15101  xblss2  15158  bdxmet  15254  xmetxp  15260  cncfcdm  15335  lgsneg  15782  lgsdilem  15785  2lgslem1a  15846  clwwlknonel  16312  clwwlknun  16321  eupth2lem2dc  16339