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  816  prlem2  977  sb6  1910  2moswapdc  2144  exsnrex  3675  eliunxp  4817  asymref  5068  elxp4  5170  elxp5  5171  dffun9  5300  funcnv  5335  funcnv3  5336  f1ompt  5731  eufnfv  5815  dff1o6  5845  abexex  6211  dfoprab4  6278  tpostpos  6350  erovlem  6714  elixp2  6789  xpsnen  6916  ctssdccl  7213  ltbtwnnq  7529  enq0enq  7544  prnmaxl  7601  prnminu  7602  elznn0nn  9386  zrevaddcl  9423  qrevaddcl  9765  climreu  11608  isprm3  12440  isprm4  12441  xpscf  13179  tgval2  14523  eltg2b  14526  isms2  14926  2lgslem1b  15566