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  576  biadani  616  orabs  821  prlem2  982  sb6  1935  2moswapdc  2170  exsnrex  3711  eliunxp  4869  asymref  5122  elxp4  5224  elxp5  5225  dffun9  5355  funcnv  5391  funcnv3  5392  f1ompt  5798  eufnfv  5884  dff1o6  5916  abexex  6287  dfoprab4  6354  tpostpos  6429  erovlem  6795  elixp2  6870  xpsnen  7004  ctssdccl  7309  ltbtwnnq  7635  enq0enq  7650  prnmaxl  7707  prnminu  7708  elznn0nn  9492  zrevaddcl  9529  qrevaddcl  9877  climreu  11857  isprm3  12689  isprm4  12690  xpscf  13429  tgval2  14774  eltg2b  14777  isms2  15177  2lgslem1b  15817