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  4768  elrnmpt1  4951  fliftf  5896  elxp7  6286  eroveu  6743  sbthlemi5  7096  sbthlemi6  7097  elfi2  7107  reapltxor  8704  divap0b  8798  nnle1eq1  9102  nn0le0eq0  9365  nn0lt10b  9495  ioopos  10114  xrmaxiflemcom  11726  fz1f1o  11852  nndivdvds  12273  dvdsmultr2  12310  bitsmod  12433  pcmpt  12832  pcmpt2  12833  resrhm2b  14178  lssle0  14301  discld  14775  cncnpi  14867  cnptoprest2  14879  lmss  14885  txcn  14914  isxmet2d  14987  xblss2  15044  bdxmet  15140  xmetxp  15146  cncfcdm  15221  lgsneg  15668  lgsdilem  15671  2lgslem1a  15732