MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71i 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 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm4.24  626  pm4.45  671  anabs1  785  2eu5  2228  imadmrn  5023  dff1o2  5442  map0e  6800  xpsnen  6941  dom0  6984  dfac5lem2  7746  pwfseqlem4  8279  axgroth6  8445  eqreznegel  10298  xrnemnf  10455  xrnepnf  10456  elioopnf  10731  elioomnf  10732  elicopnf  10733  elxrge0  10741  isprm2  12760  efgrelexlemb  15053  opsrtoslem1  16219  tgphaus  17793  ioombl1lem4  18912  vitalilem1  18957  ellogdm  19980  pjimai  22748  pm11.58  26988  bnj1101  28083
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator