Theorem pm4.71ri 633

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  biadan2  642  anabs7  808  orabs  851  prlem2  954  sb6OLD  2141  eu5  2290  2moswap  2363  exsnrex  4014  eliunxp  5077  asymref  5314  dffun9  5546  funcnv  5578  funcnv3  5579  f1ompt  5966  eufnfv  6052  dff1o6  6083  dfom2  6580  elxp4  6624  elxp5  6625  abexex  6662  dfoprab4  6733  tpostpos  6867  brwitnlem  7049  erovlem  7298  elixp2  7369  xpsnen  7497  elom3  7957  cardval2  8264  isinfcard  8365  infmap2  8490  elznn0nn  10763  zrevaddcl  10793  qrevaddcl  11078  climreu  13138  isprm3  13876  hashbc0  14170  imasleval  14583  isssc  14837  isgim  15894  eldprd  16593  eldprdOLD  16595  islmim  17251  tgval2  18679  eltg2b  18682  snfil  19555  isms2  20143  setsms  20173  elii1  20625  phtpcer  20685  elovolm  21076  ellimc2  21470  limcun  21488  1cubr  22355  fsumvma2  22671  dchrelbas3  22695  isgrpo  23820  issubgo  23927  ismgm  23944  mdsl2i  25863  cvmdi  25865  rabfmpunirn  26104  eulerpartlemn  26900  snmlval  27356  brtxp2  28048  brpprod3a  28053  prtlem100  29140  rusgranumwlks  30714  eliunxp2  30861  bnj580  32208  bnj1049  32267  islln2  33463  islpln2  33488  islvol2  33532