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  446  posng  4845  elrnmpt1  5031  fliftf  5999  elxp7  6398  eroveu  6894  sbthlemi5  7272  sbthlemi6  7273  elfi2  7300  sspw1or2  7538  reapltxor  8911  divap0b  9007  nnle1eq1  9311  nn0le0eq0  9574  nn0lt10b  9709  ioopos  10335  xrmaxiflemcom  11998  fz1f1o  12124  nndivdvds  12546  dvdsmultr2  12583  bitsmod  12706  pcmpt  13105  pcmpt2  13106  resrhm2b  14540  lssle0  14692  discld  15220  cncnpi  15312  cnptoprest2  15324  lmss  15330  txcn  15359  isxmet2d  15432  xblss2  15489  bdxmet  15585  xmetxp  15591  cncfcdm  15666  lgsneg  16126  lgsdilem  16129  2lgslem1a  16190  clwwlknonel  16656  clwwlknun  16665  eupth2lem2dc  16683