Theorem pm4.71ri 387

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  449  anabs7  546  biadani  584  orabs  786  prlem2  941  sb6  1840  2moswapdc  2065  exsnrex  3532  eliunxp  4638  asymref  4882  elxp4  4984  elxp5  4985  dffun9  5110  funcnv  5142  funcnv3  5143  f1ompt  5525  eufnfv  5602  dff1o6  5631  abexex  5978  dfoprab4  6044  tpostpos  6115  erovlem  6475  elixp2  6550  xpsnen  6668  ctssdccl  6948  ltbtwnnq  7172  enq0enq  7187  prnmaxl  7244  prnminu  7245  elznn0nn  8972  zrevaddcl  9008  qrevaddcl  9338  climreu  10958  isprm3  11645  isprm4  11646  tgval2  12063  eltg2b  12066  isms2  12443