Theorem pm4.71ri 372

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 370	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )
3	1, 2	mpbi 133	1 |- ( ph <-> ( ps /\ ph ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biadan2  429  anabs7  508  orabs  727  prlem2  881  sb6  1766  2moswapdc  1990  exsnrex  3413  eliunxp  4475  asymref  4710  elxp4  4808  elxp5  4809  dffun9  4930  funcnv  4960  funcnv3  4961  f1ompt  5320  eufnfv  5389  dff1o6  5416  abexex  5753  dfoprab4  5818  tpostpos  5879  erovlem  6198  xpsnen  6295  ltbtwnnq  6514  enq0enq  6529  prnmaxl  6586  prnminu  6587  elznn0nn  8259  zrevaddcl  8295  qrevaddcl  8578  climreu  9818