Theorem pm4.71ri 392

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 390	. 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  456  anabs7  574  biadani  612  orabs  815  prlem2  976  sb6  1898  2moswapdc  2132  exsnrex  3661  eliunxp  4802  asymref  5052  elxp4  5154  elxp5  5155  dffun9  5284  funcnv  5316  funcnv3  5317  f1ompt  5710  eufnfv  5790  dff1o6  5820  abexex  6180  dfoprab4  6247  tpostpos  6319  erovlem  6683  elixp2  6758  xpsnen  6877  ctssdccl  7172  ltbtwnnq  7478  enq0enq  7493  prnmaxl  7550  prnminu  7551  elznn0nn  9334  zrevaddcl  9370  qrevaddcl  9712  climreu  11443  isprm3  12259  isprm4  12260  xpscf  12933  tgval2  14230  eltg2b  14233  isms2  14633  2lgslem1b  15246