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  816  prlem2  977  sb6  1911  2moswapdc  2146  exsnrex  3685  eliunxp  4835  asymref  5087  elxp4  5189  elxp5  5190  dffun9  5319  funcnv  5354  funcnv3  5355  f1ompt  5754  eufnfv  5838  dff1o6  5868  abexex  6234  dfoprab4  6301  tpostpos  6373  erovlem  6737  elixp2  6812  xpsnen  6941  ctssdccl  7239  ltbtwnnq  7564  enq0enq  7579  prnmaxl  7636  prnminu  7637  elznn0nn  9421  zrevaddcl  9458  qrevaddcl  9800  climreu  11723  isprm3  12555  isprm4  12556  xpscf  13294  tgval2  14638  eltg2b  14641  isms2  15041  2lgslem1b  15681