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	|- (ph -> ps)

Assertion

Ref	Expression
pm4.71ri	|- (ph <-> (ps /\ ph))

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 |- (ph -> ps)
2		pm4.71r 612	. 2 |- ((ph -> ps) <-> (ph <-> (ps /\ ph)))
3	1, 2	mpbi 199	1 |- (ph <-> (ps /\ ph))

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  4272  dfpw12  4302  dfnnc2  4396  eliunxp  4822  elres  4996  imadmrn  5009  elxp4  5109  dffun9  5136  funcnv  5157  funcnv3  5158  dff1o6  5476  txpcofun  5804