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

Theorem pm4.71ri 614
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 612 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 199 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  biadan2  623  anabs7  785  orabs  828  prlem2  929  sb6  2112  2moswap  2292  exsnrex  3763  dfom2  4761  eliunxp  4926  asymref  5162  elxp4  5263  elxp5  5264  dffun9  5385  funcnv  5415  funcnv3  5416  f1ompt  5793  eufnfv  5872  abexex  5903  dff1o6  5913  dfoprab4  6304  tpostpos  6396  brwitnlem  6648  erovlem  6897  elixp2  6963  xpsnen  7089  elom3  7496  cardval2  7771  isinfcard  7866  infmap2  7991  elznn0nn  10188  zrevaddcl  10214  qrevaddcl  10489  climreu  12237  isprm3  12975  hashbc0  13260  imasleval  13653  isssc  13907  isgim  14936  eldprd  15449  islmim  16025  tgval2  16911  eltg2b  16914  snfil  17772  isms2  18209  setsms  18239  elii1  18648  phtpcer  18708  elovolm  19049  ellimc2  19442  limcun  19460  1cubr  20360  fsumvma2  20676  dchrelbas3  20700  isgrpo  21174  issubgo  21281  ismgm  21298  mdsl2i  23215  cvmdi  23217  rabfmpunirn  23467  snmlval  24501  brtxp2  25162  brpprod3a  25167  prtlem100  26227  bnj580  28709  bnj1049  28768  sb6NEW7  29017  anandii  29178  islln2  29771  islpln2  29796  islvol2  29840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator