Theorem pm4.71ri 643

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  biadan2  652  anabs7  824  orabs  871  prlem2  980  eu5  2335  2moswap  2386  exsnrex  4020  eliunxp  4990  asymref  5234  dffun9  5628  funcnv  5664  funcnv3  5665  f1ompt  6066  eufnfv  6163  dff1o6  6198  dfom2  6720  elxp4  6763  elxp5  6764  abexex  6802  dfoprab4  6876  tpostpos  7018  brwitnlem  7234  erovlem  7484  elixp2  7551  xpsnen  7681  elom3  8178  cardval2  8450  isinfcard  8548  infmap2  8673  elznn0nn  10979  zrevaddcl  11010  qrevaddcl  11314  hash2prb  12665  cotr2g  13088  climreu  13668  isprm3  14681  hashbc0  15005  imasleval  15495  isssc  15773  isgim  16974  eldprd  17684  brric2  18021  islmim  18333  tgval2  20019  eltg2b  20022  snfil  20927  isms2  21513  setsms  21543  elii1  22011  phtpcer  22074  elovolm  22476  ellimc2  22880  limcun  22898  1cubr  23816  fsumvma2  24190  dchrelbas3  24214  rusgranumwlks  25732  isgrpo  25972  issubgo  26079  ismgmOLD  26096  mdsl2i  28023  cvmdi  28025  rabfmpunirn  28300  eulerpartlemn  29262  bnj580  29772  bnj1049  29831  snmlval  30102  elmthm  30262  brtxp2  30696  brpprod3a  30701  prtlem100  32473  islln2  33120  islpln2  33145  islvol2  33189  elmapintrab  36226  clcnvlem  36274  eliunxp2  40387  elbigo  40634