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  576  biadani  616  orabs  821  prlem2  982  sb6  1935  2moswapdc  2170  exsnrex  3711  eliunxp  4869  asymref  5122  elxp4  5224  elxp5  5225  dffun9  5355  funcnv  5391  funcnv3  5392  f1ompt  5798  eufnfv  5885  dff1o6  5917  abexex  6288  dfoprab4  6355  tpostpos  6430  erovlem  6796  elixp2  6871  xpsnen  7005  ctssdccl  7310  ltbtwnnq  7636  enq0enq  7651  prnmaxl  7708  prnminu  7709  elznn0nn  9493  zrevaddcl  9530  qrevaddcl  9878  climreu  11862  isprm3  12695  isprm4  12696  xpscf  13435  tgval2  14781  eltg2b  14784  isms2  15184  2lgslem1b  15824