MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71ri Structured version   Visualization version   GIF version

Theorem pm4.71ri 662
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
StepHypRef Expression
1 pm4.71ri.1 . 2 (𝜑𝜓)
2 pm4.71r 660 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 218 1 (𝜑 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  biadan2  671  anabs7  847  orabs  895  prlem2  997  eu5  2479  2moswap  2530  exsnrex  4163  eliunxp  5165  asymref  5414  dffun9  5814  funcnv  5854  funcnv3  5855  f1ompt  6271  eufnfv  6369  dff1o6  6405  dfom2  6932  elxp4  6976  elxp5  6977  abexex  7015  dfoprab4  7089  tpostpos  7232  brwitnlem  7447  erovlem  7703  elixp2  7771  xpsnen  7902  elom3  8401  cardval2  8673  isinfcard  8771  infmap2  8896  elznn0nn  11220  zrevaddcl  11251  qrevaddcl  11638  hash2prb  13059  cotr2g  13505  climreu  14077  isprm3  15176  hashbc0  15489  imasleval  15966  isssc  16245  isgim  17469  eldprd  18168  brric2  18510  islmim  18825  tgval2  20509  eltg2b  20512  snfil  21416  isms2  22002  setsms  22032  elii1  22469  phtpcer  22529  phtpcerOLD  22530  elovolm  22963  ellimc2  23360  limcun  23378  1cubr  24282  fsumvma2  24652  dchrelbas3  24676  2lgslem1b  24830  rusgranumwlks  26245  isgrpo  26497  mdsl2i  28367  cvmdi  28369  rabfmpunirn  28635  eulerpartlemn  29572  bnj580  30039  bnj1049  30098  snmlval  30369  elmthm  30529  brtxp2  30960  brpprod3a  30965  ismgmOLD  32618  prtlem100  32960  islln2  33614  islpln2  33639  islvol2  33683  elmapintrab  36700  clcnvlem  36748  rusgrnumwwlks  41175  eliunxp2  41903  elbigo  42141
  Copyright terms: Public domain W3C validator