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

Theorem pm4.71ri 633
 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 631 . 2
31, 2mpbi 208 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369 This theorem is referenced by:  biadan2  642  anabs7  810  orabs  855  prlem2  963  eu5  2310  2moswap  2369  exsnrex  4067  eliunxp  5145  asymref  5388  dffun9  5621  funcnv  5653  funcnv3  5654  f1ompt  6053  eufnfv  6146  dff1o6  6181  dfom2  6702  elxp4  6744  elxp5  6745  abexex  6783  dfoprab4  6857  tpostpos  6994  brwitnlem  7176  erovlem  7426  elixp2  7493  xpsnen  7621  elom3  8086  cardval2  8393  isinfcard  8494  infmap2  8619  elznn0nn  10903  zrevaddcl  10934  qrevaddcl  11233  climreu  13379  isprm3  14226  hashbc0  14523  imasleval  14938  isssc  15189  isgim  16310  eldprd  17035  eldprdOLD  17037  brric2  17394  islmim  17708  tgval2  19457  eltg2b  19460  snfil  20365  isms2  20953  setsms  20983  elii1  21435  phtpcer  21495  elovolm  21886  ellimc2  22281  limcun  22299  1cubr  23173  fsumvma2  23489  dchrelbas3  23513  rusgranumwlks  24956  isgrpo  25198  issubgo  25305  ismgmOLD  25322  mdsl2i  27241  cvmdi  27243  rabfmpunirn  27491  eulerpartlemn  28320  snmlval  28776  elmthm  28936  brtxp2  29531  brpprod3a  29536  prtlem100  30596  eliunxp2  32923  bnj580  33971  bnj1049  34030  islln2  35235  islpln2  35260  islvol2  35304  cotr2g  37786 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 185  df-an 371
 Copyright terms: Public domain W3C validator