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

Theorem pm4.71i 627
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 625 . 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  638  pm4.45  683  anabs1  801  2eu5  2370  imadmrn  5176  dff1o2  5643  map0e  7246  xpsnen  7391  dom0  7435  dfac5lem2  8290  pwfseqlem4  8825  axgroth6  8991  eqreznegel  10936  xrnemnf  11095  xrnepnf  11096  elioopnf  11379  elioomnf  11380  elicopnf  11381  elxrge0  11390  isprm2  13767  efgrelexlemb  16240  opsrtoslem1  17541  tgphaus  19646  cfilucfil3OLD  20788  cfilucfil3  20789  ioombl1lem4  21001  vitalilem1  21047  ellogdm  22043  nb3grapr2  23297  is2wlk  23399  0spth  23405  0crct  23447  0cycl  23448  pjimai  25515  eulerpartlemt0  26682  pm11.58  29568  f12dfv  30071  erclwwlkref  30408  erclwwlknref  30424  bnj1101  31612  bj-snglc  32192
  Copyright terms: Public domain W3C validator