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  614  orabs  819  prlem2  980  sb6  1933  2moswapdc  2168  exsnrex  3708  eliunxp  4860  asymref  5113  elxp4  5215  elxp5  5216  dffun9  5346  funcnv  5381  funcnv3  5382  f1ompt  5785  eufnfv  5869  dff1o6  5899  abexex  6269  dfoprab4  6336  tpostpos  6408  erovlem  6772  elixp2  6847  xpsnen  6976  ctssdccl  7274  ltbtwnnq  7599  enq0enq  7614  prnmaxl  7671  prnminu  7672  elznn0nn  9456  zrevaddcl  9493  qrevaddcl  9835  climreu  11803  isprm3  12635  isprm4  12636  xpscf  13375  tgval2  14719  eltg2b  14722  isms2  15122  2lgslem1b  15762