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  2191  dfom2  4595  eliunxp  4776  asymref  5012  elxp4  5112  elxp5  5113  dffun9  5186  funcnv  5213  funcnv3  5214  f1ompt  5581  eufnfv  5651  abexex  5681  dff1o6  5690  dfoprab4  6076  tpostpos  6153  brwitnlem  6439  erovlem  6687  elixp2  6753  xpsnen  6879  elom3  7282  cardval2  7557  isinfcard  7652  infmap2  7777  elznn0nn  9969  zrevaddcl  9995  qrevaddcl  10270  climreu  11960  isprm3  12694  hashbc0  12979  imasleval  13370  isssc  13624  isgim  14653  eldprd  15166  islmim  15742  tgval2  16621  eltg2b  16624  snfil  17486  isms2  17923  setsms  17953  elii1  18360  phtpcer  18420  elovolm  18761  ellimc2  19154  limcun  19172  1cubr  20065  fsumvma2  20380  dchrelbas3  20404  isgrpo  20788  issubgo  20895  ismgm  20912  mdsl2i  22827  cvmdi  22829  snmlval  23251  brtxp2  23762  brpprod3a  23767  islatalg  24515  isoriso  24544  dfdir2  24623  prtlem100  26053  bnj580  27957  bnj1049  28016  anandii  28237  islln2  28830  islpln2  28855  islvol2  28899
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