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  4827  elrnmpt1  5013  fliftf  5978  elxp7  6377  eroveu  6873  sbthlemi5  7244  sbthlemi6  7245  elfi2  7272  sspw1or2  7508  reapltxor  8881  divap0b  8977  nnle1eq1  9281  nn0le0eq0  9544  nn0lt10b  9679  ioopos  10305  xrmaxiflemcom  11962  fz1f1o  12088  nndivdvds  12510  dvdsmultr2  12547  bitsmod  12670  pcmpt  13069  pcmpt2  13070  resrhm2b  14498  lssle0  14649  discld  15130  cncnpi  15222  cnptoprest2  15234  lmss  15240  txcn  15269  isxmet2d  15342  xblss2  15399  bdxmet  15495  xmetxp  15501  cncfcdm  15576  lgsneg  16026  lgsdilem  16029  2lgslem1a  16090  clwwlknonel  16556  clwwlknun  16565  eupth2lem2dc  16583