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  2385  imadmrn  5338  dff1o2  5812  f12dfv  6158  map0e  7446  xpsnen  7591  dom0  7635  dfac5lem2  8494  pwfseqlem4  9029  axgroth6  9195  eqreznegel  11156  xrnemnf  11317  xrnepnf  11318  elioopnf  11607  elioomnf  11608  elicopnf  11609  elxrge0  11618  isprm2  14073  efgrelexlemb  16557  opsrtoslem1  17912  tgphaus  20343  cfilucfil3OLD  21485  cfilucfil3  21486  ioombl1lem4  21699  vitalilem1  21745  ellogdm  22741  nb3grapr2  24116  is2wlk  24229  0spth  24235  0crct  24288  0cycl  24289  erclwwlkref  24475  erclwwlknref  24487  pjimai  26757  eulerpartlemt0  27934  pm11.58  30829  bnj1101  32797  bj-snglc  33483
  Copyright terms: Public domain W3C validator