Theorem pm4.71ri 614

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 612	. 2 ⊢ ((φ → ψ) ↔ (φ ↔ (ψ ∧ φ)))
3	1, 2	mpbi 199	1 ⊢ (φ ↔ (ψ ∧ φ))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  biadan2  623  anabs7  785  orabs  828  prlem2  929  sb6  2099  2moswap  2279  opkelimagekg  4271  dfpw12  4301  dfnnc2  4395  eliunxp  4821  elres  4995  imadmrn  5008  elxp4  5108  dffun9  5135  funcnv  5156  funcnv3  5157  dff1o6  5475  txpcofun  5803