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  2219  dfom2  4657  eliunxp  4822  asymref  5058  elxp4  5158  elxp5  5159  dffun9  5248  funcnv  5276  funcnv3  5277  f1ompt  5644  eufnfv  5714  abexex  5744  dff1o6  5753  dfoprab4  6139  tpostpos  6216  brwitnlem  6502  erovlem  6750  elixp2  6816  xpsnen  6942  elom3  7345  cardval2  7620  isinfcard  7715  infmap2  7840  elznn0nn  10033  zrevaddcl  10059  qrevaddcl  10334  climreu  12026  isprm3  12763  hashbc0  13048  imasleval  13439  isssc  13693  isgim  14722  eldprd  15235  islmim  15811  tgval2  16690  eltg2b  16693  snfil  17555  isms2  17992  setsms  18022  elii1  18429  phtpcer  18489  elovolm  18830  ellimc2  19223  limcun  19241  1cubr  20134  fsumvma2  20449  dchrelbas3  20473  isgrpo  20857  issubgo  20964  ismgm  20981  mdsl2i  22898  cvmdi  22900  snmlval  23321  brtxp2  23832  brpprod3a  23837  islatalg  24594  isoriso  24623  dfdir2  24702  prtlem100  26132  bnj580  28224  bnj1049  28283  anandii  28386  islln2  28979  islpln2  29004  islvol2  29048
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