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 664
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 662 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 220 1 (𝜑 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  biadan2  673  anabs7  851  orabs  899  prlem2  1005  eu5  2495  2moswap  2546  exsnrex  4199  eliunxp  5229  asymref  5481  dffun9  5886  funcnv  5926  funcnv3  5927  f1ompt  6348  eufnfv  6456  dff1o6  6496  dfom2  7029  elxp4  7072  elxp5  7073  abexex  7111  dfoprab4  7185  tpostpos  7332  brwitnlem  7547  erovlem  7803  elixp2  7872  xpsnen  8004  elom3  8505  cardval2  8777  isinfcard  8875  infmap2  9000  elznn0nn  11351  zrevaddcl  11382  qrevaddcl  11770  hash2prb  13208  cotr2g  13665  climreu  14237  isprm3  15339  hashbc0  15652  imasleval  16141  isssc  16420  isgim  17644  eldprd  18343  brric2  18685  islmim  19002  tgval2  20700  eltg2b  20703  snfil  21608  isms2  22195  setsms  22225  elii1  22674  phtpcer  22734  phtpcerOLD  22735  elovolm  23183  ellimc2  23581  limcun  23599  1cubr  24503  fsumvma2  24873  dchrelbas3  24897  2lgslem1b  25051  rusgrnumwwlks  26770  isgrpo  27239  mdsl2i  29069  cvmdi  29071  rabfmpunirn  29336  eulerpartlemn  30266  bnj580  30744  bnj1049  30803  snmlval  31074  elmthm  31234  brtxp2  31683  brpprod3a  31688  ismgmOLD  33320  prtlem100  33662  islln2  34316  islpln2  34341  islvol2  34385  elmapintrab  37402  clcnvlem  37450  sprvalpw  41048  sprvalpwn0  41051  eliunxp2  41430  elbigo  41667
  Copyright terms: Public domain W3C validator