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

Theorem pm4.71i 632
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
Hypothesis
Ref Expression
pm4.71i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm4.71i  |-  ( ph  <->  (
ph  /\  ps )
)

Proof of Theorem pm4.71i
StepHypRef Expression
1 pm4.71i.1 . 2  |-  ( ph  ->  ps )
2 pm4.71 630 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
31, 2mpbi 208 1  |-  ( ph  <->  (
ph  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm4.24  643  pm4.45  688  anabs1  806  2eu5  2370  imadmrn  5179  dff1o2  5646  map0e  7250  xpsnen  7395  dom0  7439  dfac5lem2  8294  pwfseqlem4  8829  axgroth6  8995  eqreznegel  10940  xrnemnf  11099  xrnepnf  11100  elioopnf  11383  elioomnf  11384  elicopnf  11385  elxrge0  11394  isprm2  13771  efgrelexlemb  16247  opsrtoslem1  17565  tgphaus  19687  cfilucfil3OLD  20829  cfilucfil3  20830  ioombl1lem4  21042  vitalilem1  21088  ellogdm  22084  nb3grapr2  23362  is2wlk  23464  0spth  23470  0crct  23512  0cycl  23513  pjimai  25580  eulerpartlemt0  26752  pm11.58  29643  f12dfv  30146  erclwwlkref  30483  erclwwlknref  30499  bnj1101  31778  bj-snglc  32462
  Copyright terms: Public domain W3C validator