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  4864  asymref  5117  elxp4  5219  elxp5  5220  dffun9  5350  funcnv  5385  funcnv3  5386  f1ompt  5791  eufnfv  5877  dff1o6  5909  abexex  6280  dfoprab4  6347  tpostpos  6421  erovlem  6787  elixp2  6862  xpsnen  6993  ctssdccl  7294  ltbtwnnq  7619  enq0enq  7634  prnmaxl  7691  prnminu  7692  elznn0nn  9476  zrevaddcl  9513  qrevaddcl  9856  climreu  11829  isprm3  12661  isprm4  12662  xpscf  13401  tgval2  14746  eltg2b  14749  isms2  15149  2lgslem1b  15789