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 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

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:  biadan2  460  anabs7  580  biadani  620  orabs  826  prlem2  987  sb6  1941  2moswapdc  2177  exsnrex  3747  eliunxp  4914  asymref  5168  elxp4  5270  elxp5  5271  dffun9  5401  funcnv  5437  funcnv3  5438  f1ompt  5850  eufnfv  5939  dff1o6  5972  abexex  6345  dfoprab4  6416  tpostpos  6525  erovlem  6891  elixp2  6974  xpsnen  7109  ctssdccl  7441  ltbtwnnq  7773  enq0enq  7788  prnmaxl  7845  prnminu  7846  elznn0nn  9637  zrevaddcl  9674  qrevaddcl  10023  climreu  12041  isprm3  12874  isprm4  12875  xpscf  13645  tgval2  15075  eltg2b  15078  isms2  15478  2lgslem1b  16122