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  614  orabs  819  prlem2  980  sb6  1933  2moswapdc  2168  exsnrex  3709  eliunxp  4867  asymref  5120  elxp4  5222  elxp5  5223  dffun9  5353  funcnv  5388  funcnv3  5389  f1ompt  5794  eufnfv  5880  dff1o6  5912  abexex  6283  dfoprab4  6350  tpostpos  6425  erovlem  6791  elixp2  6866  xpsnen  7000  ctssdccl  7301  ltbtwnnq  7626  enq0enq  7641  prnmaxl  7698  prnminu  7699  elznn0nn  9483  zrevaddcl  9520  qrevaddcl  9868  climreu  11848  isprm3  12680  isprm4  12681  xpscf  13420  tgval2  14765  eltg2b  14768  isms2  15168  2lgslem1b  15808