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

Theorem pm4.71ri 615
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 613 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 200 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biadan2  624  anabs7  786  orabs  829  prlem2  930  sb6  2132  2moswap  2313  exsnrex  3791  dfom2  4787  eliunxp  4952  asymref  5190  elxp4  5297  elxp5  5298  dffun9  5421  funcnv  5451  funcnv3  5452  f1ompt  5830  eufnfv  5911  abexex  5942  dff1o6  5952  dfoprab4  6343  tpostpos  6435  brwitnlem  6687  erovlem  6936  elixp2  7002  xpsnen  7128  elom3  7536  cardval2  7811  isinfcard  7906  infmap2  8031  elznn0nn  10227  zrevaddcl  10253  qrevaddcl  10528  climreu  12277  isprm3  13015  hashbc0  13300  imasleval  13693  isssc  13947  isgim  14976  eldprd  15489  islmim  16061  tgval2  16944  eltg2b  16947  snfil  17817  isms2  18370  setsms  18400  elii1  18831  phtpcer  18891  elovolm  19238  ellimc2  19631  limcun  19649  1cubr  20549  fsumvma2  20865  dchrelbas3  20889  isgrpo  21632  issubgo  21739  ismgm  21756  mdsl2i  23673  cvmdi  23675  rabfmpunirn  23907  snmlval  24797  brtxp2  25445  brpprod3a  25450  prtlem100  26395  bnj580  28622  bnj1049  28681  sb6NEW7  28930  islln2  29625  islpln2  29650  islvol2  29694
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 178  df-an 361
  Copyright terms: Public domain W3C validator