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  2040  2moswap  2220  dfom2  4660  eliunxp  4825  asymref  5061  elxp4  5162  elxp5  5163  dffun9  5284  funcnv  5312  funcnv3  5313  f1ompt  5684  eufnfv  5754  abexex  5784  dff1o6  5793  dfoprab4  6179  tpostpos  6256  brwitnlem  6508  erovlem  6756  elixp2  6822  xpsnen  6948  elom3  7351  cardval2  7626  isinfcard  7721  infmap2  7846  elznn0nn  10039  zrevaddcl  10065  qrevaddcl  10340  climreu  12032  isprm3  12769  hashbc0  13054  imasleval  13445  isssc  13699  isgim  14728  eldprd  15241  islmim  15817  tgval2  16696  eltg2b  16699  snfil  17561  isms2  17998  setsms  18028  elii1  18435  phtpcer  18495  elovolm  18836  ellimc2  19229  limcun  19247  1cubr  20140  fsumvma2  20455  dchrelbas3  20479  isgrpo  20865  issubgo  20972  ismgm  20989  mdsl2i  22904  cvmdi  22906  rabfmpunirn  23219  snmlval  23916  brtxp2  24423  brpprod3a  24428  islatalg  25194  isoriso  25223  dfdir2  25302  prtlem100  26732  bnj580  29018  bnj1049  29077  anandii  29180  islln2  29773  islpln2  29798  islvol2  29842
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