Theorem pm4.71ri 396

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadan2  460  anabs7  580  biadani  620  orabs  826  prlem2  987  sb6  1941  2moswapdc  2177  exsnrex  3751  eliunxp  4919  asymref  5173  elxp4  5275  elxp5  5276  dffun9  5406  funcnv  5442  funcnv3  5443  f1ompt  5859  eufnfv  5949  dff1o6  5982  abexex  6355  dfoprab4  6426  tpostpos  6535  erovlem  6901  elixp2  6984  xpsnen  7119  ctssdccl  7451  ltbtwnnq  7783  enq0enq  7798  prnmaxl  7855  prnminu  7856  elznn0nn  9658  zrevaddcl  9695  qrevaddcl  10044  climreu  12063  isprm3  12896  isprm4  12897  xpscf  13668  tgval2  15152  eltg2b  15155  isms2  15555  2lgslem1b  16208