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  8635  divap0b  8729  nnle1eq1  9033  nn0le0eq0  9296  nn0lt10b  9425  ioopos  10044  xrmaxiflemcom  11433  fz1f1o  11559  nndivdvds  11980  dvdsmultr2  12017  bitsmod  12140  pcmpt  12539  pcmpt2  12540  resrhm2b  13883  lssle0  14006  discld  14458  cncnpi  14550  cnptoprest2  14562  lmss  14568  txcn  14597  isxmet2d  14670  xblss2  14727  bdxmet  14823  xmetxp  14829  cncfcdm  14904  lgsneg  15351  lgsdilem  15354  2lgslem1a  15415