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

Theorem pm4.71i 615
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 613 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  (
ph  /\  ps )
) )
31, 2mpbi 201 1  |-  ( ph  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm4.24  626  pm4.45  671  anabs1  785  2eu5  2367  imadmrn  5217  dff1o2  5681  map0e  7053  xpsnen  7194  dom0  7237  dfac5lem2  8007  pwfseqlem4  8539  axgroth6  8705  eqreznegel  10563  xrnemnf  10720  xrnepnf  10721  elioopnf  11000  elioomnf  11001  elicopnf  11002  elxrge0  11010  isprm2  13089  efgrelexlemb  15384  opsrtoslem1  16546  tgphaus  18148  cfilucfil3OLD  19273  cfilucfil3  19274  ioombl1lem4  19457  vitalilem1  19502  ellogdm  20532  nb3grapr2  21465  is2wlk  21567  0spth  21573  0crct  21615  0cycl  21616  pjimai  23681  pm11.58  27568  f12dfv  28082  bnj1101  29157
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator