Theorem pm4.71ri 385

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  445  anabs7  542  biadani  580  orabs  766  prlem2  923  sb6  1821  2moswapdc  2045  exsnrex  3505  eliunxp  4606  asymref  4850  elxp4  4952  elxp5  4953  dffun9  5078  funcnv  5109  funcnv3  5110  f1ompt  5489  eufnfv  5564  dff1o6  5593  abexex  5935  dfoprab4  6000  tpostpos  6067  erovlem  6424  elixp2  6499  xpsnen  6617  ltbtwnnq  7072  enq0enq  7087  prnmaxl  7144  prnminu  7145  elznn0nn  8862  zrevaddcl  8898  qrevaddcl  9228  climreu  10840  isprm3  11527  isprm4  11528  tgval2  11903  eltg2b  11906  isms2  12240