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  612  orabs  815  prlem2  976  sb6  1901  2moswapdc  2135  exsnrex  3665  eliunxp  4806  asymref  5056  elxp4  5158  elxp5  5159  dffun9  5288  funcnv  5320  funcnv3  5321  f1ompt  5716  eufnfv  5796  dff1o6  5826  abexex  6192  dfoprab4  6259  tpostpos  6331  erovlem  6695  elixp2  6770  xpsnen  6889  ctssdccl  7186  ltbtwnnq  7502  enq0enq  7517  prnmaxl  7574  prnminu  7575  elznn0nn  9359  zrevaddcl  9395  qrevaddcl  9737  climreu  11481  isprm3  12313  isprm4  12314  xpscf  13051  tgval2  14395  eltg2b  14398  isms2  14798  2lgslem1b  15438