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  614  orabs  819  prlem2  980  sb6  1933  2moswapdc  2168  exsnrex  3708  eliunxp  4861  asymref  5114  elxp4  5216  elxp5  5217  dffun9  5347  funcnv  5382  funcnv3  5383  f1ompt  5786  eufnfv  5870  dff1o6  5900  abexex  6271  dfoprab4  6338  tpostpos  6410  erovlem  6774  elixp2  6849  xpsnen  6980  ctssdccl  7278  ltbtwnnq  7603  enq0enq  7618  prnmaxl  7675  prnminu  7676  elznn0nn  9460  zrevaddcl  9497  qrevaddcl  9839  climreu  11808  isprm3  12640  isprm4  12641  xpscf  13380  tgval2  14725  eltg2b  14728  isms2  15128  2lgslem1b  15768