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  4736  elrnmpt1  4918  fliftf  5849  elxp7  6237  eroveu  6694  sbthlemi5  7036  sbthlemi6  7037  elfi2  7047  reapltxor  8633  divap0b  8727  nnle1eq1  9031  nn0le0eq0  9294  nn0lt10b  9423  ioopos  10042  xrmaxiflemcom  11431  fz1f1o  11557  nndivdvds  11978  dvdsmultr2  12015  bitsmod  12138  pcmpt  12537  pcmpt2  12538  resrhm2b  13881  lssle0  14004  discld  14456  cncnpi  14548  cnptoprest2  14560  lmss  14566  txcn  14595  isxmet2d  14668  xblss2  14725  bdxmet  14821  xmetxp  14827  cncfcdm  14902  lgsneg  15349  lgsdilem  15352  2lgslem1a  15413