Theorem pm4.71ri 564

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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
pm4.71ri	⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	pm4.71i 563	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 466	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anabs7  663  biadaniALT  820  orabs  996  prlem2  1051  dfeumo  2554  dfeu  2615  2moswapv  2650  2moswap  2665  exsnrex  4578  eliunxp  5683  asymref  5953  dffun9  6369  funcnv  6409  funcnv3  6410  f1ompt  6872  eufnfv  6989  dff1o6  7030  dfom2  7587  elxp4  7638  elxp5  7639  abexex  7682  dfoprab4  7763  tpostpos  7928  brwitnlem  8148  erovlem  8409  elixp2  8496  xpsnen  8635  elom3  9157  cardval2  9466  isinfcard  9565  infmap2  9691  elznn0nn  12047  zrevaddcl  12079  qrevaddcl  12424  hash2prb  13895  cotr2g  14396  climreu  14974  isprm3  16092  hashbc0  16409  imasleval  16885  xpscf  16909  isssc  17162  issubmndb  18049  isgim  18482  eldprd  19207  brric2  19581  islmim  19915  tgval2  21669  eltg2b  21672  snfil  22577  isms2  23165  setsms  23195  elii1  23649  phtpcer  23709  elovolm  24188  ellimc2  24589  limcun  24607  1cubr  25540  fsumvma2  25910  dchrelbas3  25934  2lgslem1b  26088  nbgrel  27242  rusgrnumwwlks  27872  isgrpo  28392  mdsl2i  30217  cvmdi  30219  rabfmpunirn  30526  zarcls  31357  eulerpartlemn  31879  bnj580  32425  bnj1049  32486  snmlval  32821  satf0suclem  32865  fmlasuc0  32874  elmthm  33066  imaindm  33281  dmscut  33600  madeval2  33631  made0  33648  brtxp2  33766  brpprod3a  33771  bj-elid6  34899  ismgmOLD  35602  brres2  36003  brxrn2  36101  redundpim3  36339  prtlem100  36469  islln2  37121  islpln2  37146  islvol2  37190  prjspeclsp  39983  en2pr  40654  pren2  40660  elmapintrab  40684  clcnvlem  40731  sprvalpw  44414  sprvalpwn0  44417  prprvalpw  44449  eliunxp2  45151  elbigo  45379