MPE Home 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  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm4.71ri  |-  ( ph  <->  ( ps  /\  ph )
)

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2  |-  ( ph  ->  ps )
2 pm4.71r 615 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 201 1  |-  ( ph  <->  ( ps  /\  ph )
)
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  1993  2moswap  2193  dfom2  4630  eliunxp  4811  asymref  5047  elxp4  5147  elxp5  5148  dffun9  5221  funcnv  5248  funcnv3  5249  f1ompt  5616  eufnfv  5686  abexex  5716  dff1o6  5725  dfoprab4  6111  tpostpos  6188  brwitnlem  6474  erovlem  6722  elixp2  6788  xpsnen  6914  elom3  7317  cardval2  7592  isinfcard  7687  infmap2  7812  elznn0nn  10005  zrevaddcl  10031  qrevaddcl  10306  climreu  11996  isprm3  12730  hashbc0  13015  imasleval  13406  isssc  13660  isgim  14689  eldprd  15202  islmim  15778  tgval2  16657  eltg2b  16660  snfil  17522  isms2  17959  setsms  17989  elii1  18396  phtpcer  18456  elovolm  18797  ellimc2  19190  limcun  19208  1cubr  20101  fsumvma2  20416  dchrelbas3  20440  isgrpo  20824  issubgo  20931  ismgm  20948  mdsl2i  22863  cvmdi  22865  snmlval  23287  brtxp2  23798  brpprod3a  23803  islatalg  24551  isoriso  24580  dfdir2  24659  prtlem100  26089  bnj580  28077  bnj1049  28136  anandii  28357  islln2  28950  islpln2  28975  islvol2  29019
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