Theorem pm4.71ri 390

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 388	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 144	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  453  anabs7  569  biadani  607  orabs  809  prlem2  969  sb6  1879  2moswapdc  2109  exsnrex  3625  eliunxp  4750  asymref  4996  elxp4  5098  elxp5  5099  dffun9  5227  funcnv  5259  funcnv3  5260  f1ompt  5647  eufnfv  5726  dff1o6  5755  abexex  6105  dfoprab4  6171  tpostpos  6243  erovlem  6605  elixp2  6680  xpsnen  6799  ctssdccl  7088  ltbtwnnq  7378  enq0enq  7393  prnmaxl  7450  prnminu  7451  elznn0nn  9226  zrevaddcl  9262  qrevaddcl  9603  climreu  11260  isprm3  12072  isprm4  12073  tgval2  12845  eltg2b  12848  isms2  13248