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  810  orabs  855  prlem2  963  eu5  2311  2moswap  2369  exsnrex  4070  eliunxp  5150  asymref  5393  dffun9  5622  funcnv  5654  funcnv3  5655  f1ompt  6054  eufnfv  6147  dff1o6  6182  dfom2  6701  elxp4  6743  elxp5  6744  abexex  6782  dfoprab4  6856  tpostpos  6993  brwitnlem  7175  erovlem  7425  elixp2  7492  xpsnen  7620  elom3  8082  cardval2  8389  isinfcard  8490  infmap2  8615  elznn0nn  10899  zrevaddcl  10930  qrevaddcl  11229  climreu  13391  isprm3  14238  hashbc0  14535  imasleval  14958  isssc  15236  isgim  16437  eldprd  17162  eldprdOLD  17164  brric2  17521  islmim  17835  tgval2  19584  eltg2b  19587  snfil  20491  isms2  21079  setsms  21109  elii1  21561  phtpcer  21621  elovolm  22012  ellimc2  22407  limcun  22425  1cubr  23299  fsumvma2  23615  dchrelbas3  23639  rusgranumwlks  25083  isgrpo  25325  issubgo  25432  ismgmOLD  25449  mdsl2i  27368  cvmdi  27370  rabfmpunirn  27639  eulerpartlemn  28517  snmlval  28973  elmthm  29133  brtxp2  29736  brpprod3a  29741  prtlem100  30801  eliunxp2  33067  bnj580  34114  bnj1049  34173  islln2  35378  islpln2  35403  islvol2  35447  cotr2g  37952