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

Theorem pm4.71i 630
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 628 . 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 367
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 369
This theorem is referenced by:  pm4.24  641  pm4.45  686  anabs1  806  2eu5  2379  imadmrn  5335  dff1o2  5803  f12dfv  6154  xpsnen  7594  dom0  7638  dfac5lem2  8496  pwfseqlem4  9029  axgroth6  9195  eqreznegel  11168  xrnemnf  11331  xrnepnf  11332  elioopnf  11621  elioomnf  11622  elicopnf  11623  elxrge0  11632  isprm2  14309  efgrelexlemb  16967  opsrtoslem1  18343  tgphaus  20781  cfilucfil3OLD  21923  cfilucfil3  21924  ioombl1lem4  22137  vitalilem1  22183  ellogdm  23188  nb3grapr2  24656  is2wlk  24769  0spth  24775  0crct  24828  0cycl  24829  erclwwlkref  25015  erclwwlknref  25027  pjimai  27293  dfrp2  27815  eulerpartlemt0  28572  wl-cases2-dnf  30210  pm11.58  31537  bnj1101  34244  bj-snglc  34928
  Copyright terms: Public domain W3C validator