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  2366  imadmrn  5333  dff1o2  5807  f12dfv  6160  xpsnen  7599  dom0  7643  dfac5lem2  8503  pwfseqlem4  9038  axgroth6  9204  eqreznegel  11171  xrnemnf  11332  xrnepnf  11333  elioopnf  11622  elioomnf  11623  elicopnf  11624  elxrge0  11633  isprm2  14097  efgrelexlemb  16637  opsrtoslem1  18016  tgphaus  20481  cfilucfil3OLD  21623  cfilucfil3  21624  ioombl1lem4  21837  vitalilem1  21883  ellogdm  22885  nb3grapr2  24319  is2wlk  24432  0spth  24438  0crct  24491  0cycl  24492  erclwwlkref  24678  erclwwlknref  24690  pjimai  26960  eulerpartlemt0  28174  pm11.58  31243  bnj1101  33550  bj-snglc  34239
  Copyright terms: Public domain W3C validator