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  1910  2moswapdc  2144  exsnrex  3675  eliunxp  4818  asymref  5069  elxp4  5171  elxp5  5172  dffun9  5301  funcnv  5336  funcnv3  5337  f1ompt  5733  eufnfv  5817  dff1o6  5847  abexex  6213  dfoprab4  6280  tpostpos  6352  erovlem  6716  elixp2  6791  xpsnen  6918  ctssdccl  7215  ltbtwnnq  7531  enq0enq  7546  prnmaxl  7603  prnminu  7604  elznn0nn  9388  zrevaddcl  9425  qrevaddcl  9767  climreu  11641  isprm3  12473  isprm4  12474  xpscf  13212  tgval2  14556  eltg2b  14559  isms2  14959  2lgslem1b  15599