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  2038  2moswap  2218  dfom2  4658  eliunxp  4823  asymref  5059  elxp4  5160  elxp5  5161  dffun9  5282  funcnv  5310  funcnv3  5311  f1ompt  5682  eufnfv  5752  abexex  5782  dff1o6  5791  dfoprab4  6177  tpostpos  6254  brwitnlem  6506  erovlem  6754  elixp2  6820  xpsnen  6946  elom3  7349  cardval2  7624  isinfcard  7719  infmap2  7844  elznn0nn  10037  zrevaddcl  10063  qrevaddcl  10338  climreu  12030  isprm3  12767  hashbc0  13052  imasleval  13443  isssc  13697  isgim  14726  eldprd  15239  islmim  15815  tgval2  16694  eltg2b  16697  snfil  17559  isms2  17996  setsms  18026  elii1  18433  phtpcer  18493  elovolm  18834  ellimc2  19227  limcun  19245  1cubr  20138  fsumvma2  20453  dchrelbas3  20477  isgrpo  20863  issubgo  20970  ismgm  20987  mdsl2i  22902  cvmdi  22904  rabfmpunirn  23217  snmlval  23914  brtxp2  24421  brpprod3a  24426  islatalg  25183  isoriso  25212  dfdir2  25291  prtlem100  26721  bnj580  28945  bnj1049  29004  anandii  29107  islln2  29700  islpln2  29725  islvol2  29769
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