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  814  prlem2  974  sb6  1886  2moswapdc  2116  exsnrex  3636  eliunxp  4768  asymref  5016  elxp4  5118  elxp5  5119  dffun9  5247  funcnv  5279  funcnv3  5280  f1ompt  5669  eufnfv  5749  dff1o6  5779  abexex  6129  dfoprab4  6195  tpostpos  6267  erovlem  6629  elixp2  6704  xpsnen  6823  ctssdccl  7112  ltbtwnnq  7417  enq0enq  7432  prnmaxl  7489  prnminu  7490  elznn0nn  9269  zrevaddcl  9305  qrevaddcl  9646  climreu  11307  isprm3  12120  isprm4  12121  xpscf  12771  tgval2  13590  eltg2b  13593  isms2  13993