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  4791  elrnmpt1  4975  fliftf  5929  elxp7  6322  eroveu  6781  sbthlemi5  7136  sbthlemi6  7137  elfi2  7147  reapltxor  8744  divap0b  8838  nnle1eq1  9142  nn0le0eq0  9405  nn0lt10b  9535  ioopos  10154  xrmaxiflemcom  11768  fz1f1o  11894  nndivdvds  12315  dvdsmultr2  12352  bitsmod  12475  pcmpt  12874  pcmpt2  12875  resrhm2b  14221  lssle0  14344  discld  14818  cncnpi  14910  cnptoprest2  14922  lmss  14928  txcn  14957  isxmet2d  15030  xblss2  15087  bdxmet  15183  xmetxp  15189  cncfcdm  15264  lgsneg  15711  lgsdilem  15714  2lgslem1a  15775