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

Theorem pm4.71ri 617
 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 615 . 2
31, 2mpbi 201 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360 This theorem is referenced by:  biadan2  626  anabs7  788  orabs  831  prlem2  934  sb6  1992  2moswap  2188  dfom2  4549  eliunxp  4730  asymref  4966  elxp4  5066  elxp5  5067  dffun9  5140  funcnv  5167  funcnv3  5168  f1ompt  5534  eufnfv  5604  abexex  5634  dff1o6  5643  dfoprab4  6029  tpostpos  6106  brwitnlem  6392  erovlem  6640  elixp2  6706  xpsnen  6831  elom3  7233  cardval2  7508  isinfcard  7603  infmap2  7728  elznn0nn  9916  zrevaddcl  9942  qrevaddcl  10217  climreu  11907  isprm3  12641  hashbc0  12926  imasleval  13317  isssc  13541  isgim  14561  eldprd  15074  islmim  15650  tgval2  16526  eltg2b  16529  snfil  17391  isms2  17828  setsms  17858  elii1  18265  phtpcer  18325  elovolm  18666  ellimc2  19059  limcun  19077  1cubr  19970  fsumvma2  20285  dchrelbas3  20309  isgrpo  20693  issubgo  20800  ismgm  20817  mdsl2i  22732  cvmdi  22734  snmlval  23085  brtxp2  23596  brpprod3a  23601  islatalg  24349  isoriso  24378  dfdir2  24457  prtlem100  25887  bnj580  27634  bnj1049  27693  anandii  27796  islln2  28389  islpln2  28414  islvol2  28458 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10 This theorem depends on definitions:  df-bi 179  df-an 362
 Copyright terms: Public domain W3C validator