Theorem pm4.71ri 396

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)

Hypothesis

Ref	Expression
pm4.71ri.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
pm4.71ri	⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 ⊢ (𝜑 → 𝜓)
2		pm4.71r 394	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 145	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadan2  460  anabs7  580  biadani  620  orabs  826  prlem2  987  sb6  1941  2moswapdc  2177  exsnrex  3751  eliunxp  4921  asymref  5176  elxp4  5278  elxp5  5279  dffun9  5409  funcnv  5445  funcnv3  5446  f1ompt  5862  eufnfv  5952  dff1o6  5985  abexex  6359  dfoprab4  6430  tpostpos  6539  erovlem  6905  elixp2  6988  xpsnen  7123  ctssdccl  7457  ltbtwnnq  7789  enq0enq  7804  prnmaxl  7861  prnminu  7862  elznn0nn  9669  zrevaddcl  9706  qrevaddcl  10060  climreu  12088  isprm3  12921  isprm4  12922  xpscf  13727  tgval2  15277  eltg2b  15280  isms2  15680  2lgslem1b  16413