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

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  815  prlem2  976  sb6  1901  2moswapdc  2135  exsnrex  3664  eliunxp  4805  asymref  5055  elxp4  5157  elxp5  5158  dffun9  5287  funcnv  5319  funcnv3  5320  f1ompt  5713  eufnfv  5793  dff1o6  5823  abexex  6183  dfoprab4  6250  tpostpos  6322  erovlem  6686  elixp2  6761  xpsnen  6880  ctssdccl  7177  ltbtwnnq  7483  enq0enq  7498  prnmaxl  7555  prnminu  7556  elznn0nn  9340  zrevaddcl  9376  qrevaddcl  9718  climreu  11462  isprm3  12286  isprm4  12287  xpscf  12990  tgval2  14287  eltg2b  14290  isms2  14690  2lgslem1b  15330