Theorem pm4.71ri 390

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 388	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 144	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  452  anabs7  564  biadani  602  orabs  804  prlem2  959  sb6  1859  2moswapdc  2090  exsnrex  3573  eliunxp  4686  asymref  4932  elxp4  5034  elxp5  5035  dffun9  5160  funcnv  5192  funcnv3  5193  f1ompt  5579  eufnfv  5656  dff1o6  5685  abexex  6032  dfoprab4  6098  tpostpos  6169  erovlem  6529  elixp2  6604  xpsnen  6723  ctssdccl  7004  ltbtwnnq  7248  enq0enq  7263  prnmaxl  7320  prnminu  7321  elznn0nn  9092  zrevaddcl  9128  qrevaddcl  9463  climreu  11098  isprm3  11835  isprm4  11836  tgval2  12259  eltg2b  12262  isms2  12662