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  1898  2moswapdc  2132  exsnrex  3660  eliunxp  4801  asymref  5051  elxp4  5153  elxp5  5154  dffun9  5283  funcnv  5315  funcnv3  5316  f1ompt  5709  eufnfv  5789  dff1o6  5819  abexex  6178  dfoprab4  6245  tpostpos  6317  erovlem  6681  elixp2  6756  xpsnen  6875  ctssdccl  7170  ltbtwnnq  7476  enq0enq  7491  prnmaxl  7548  prnminu  7549  elznn0nn  9331  zrevaddcl  9367  qrevaddcl  9709  climreu  11440  isprm3  12256  isprm4  12257  xpscf  12930  tgval2  14219  eltg2b  14222  isms2  14622