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  1909  2moswapdc  2143  exsnrex  3674  eliunxp  4816  asymref  5067  elxp4  5169  elxp5  5170  dffun9  5299  funcnv  5334  funcnv3  5335  f1ompt  5730  eufnfv  5814  dff1o6  5844  abexex  6210  dfoprab4  6277  tpostpos  6349  erovlem  6713  elixp2  6788  xpsnen  6915  ctssdccl  7212  ltbtwnnq  7528  enq0enq  7543  prnmaxl  7600  prnminu  7601  elznn0nn  9385  zrevaddcl  9422  qrevaddcl  9764  climreu  11550  isprm3  12382  isprm4  12383  xpscf  13121  tgval2  14465  eltg2b  14468  isms2  14868  2lgslem1b  15508