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  4731  elrnmpt1  4913  fliftf  5842  elxp7  6223  eroveu  6680  sbthlemi5  7020  sbthlemi6  7021  elfi2  7031  reapltxor  8608  divap0b  8702  nnle1eq1  9006  nn0le0eq0  9268  nn0lt10b  9397  ioopos  10016  xrmaxiflemcom  11392  fz1f1o  11518  nndivdvds  11939  dvdsmultr2  11976  pcmpt  12481  pcmpt2  12482  resrhm2b  13745  lssle0  13868  discld  14304  cncnpi  14396  cnptoprest2  14408  lmss  14414  txcn  14443  isxmet2d  14516  xblss2  14573  bdxmet  14669  xmetxp  14675  cncfcdm  14737  lgsneg  15140  lgsdilem  15143