Theorem pm4.71ri 396

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadan2  460  anabs7  580  biadani  620  orabs  826  prlem2  987  sb6  1941  2moswapdc  2177  exsnrex  3751  eliunxp  4919  asymref  5173  elxp4  5275  elxp5  5276  dffun9  5406  funcnv  5442  funcnv3  5443  f1ompt  5859  eufnfv  5949  dff1o6  5982  abexex  6355  dfoprab4  6426  tpostpos  6535  erovlem  6901  elixp2  6984  xpsnen  7119  ctssdccl  7452  ltbtwnnq  7784  enq0enq  7799  prnmaxl  7856  prnminu  7857  elznn0nn  9663  zrevaddcl  9700  qrevaddcl  10054  climreu  12082  isprm3  12915  isprm4  12916  xpscf  13721  tgval2  15243  eltg2b  15246  isms2  15646  2lgslem1b  16374