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  815  prlem2  976  sb6  1898  2moswapdc  2128  exsnrex  3649  eliunxp  4781  asymref  5029  elxp4  5131  elxp5  5132  dffun9  5260  funcnv  5292  funcnv3  5293  f1ompt  5683  eufnfv  5763  dff1o6  5793  abexex  6145  dfoprab4  6211  tpostpos  6283  erovlem  6645  elixp2  6720  xpsnen  6839  ctssdccl  7128  ltbtwnnq  7433  enq0enq  7448  prnmaxl  7505  prnminu  7506  elznn0nn  9285  zrevaddcl  9321  qrevaddcl  9662  climreu  11323  isprm3  12136  isprm4  12137  xpscf  12789  tgval2  13948  eltg2b  13951  isms2  14351