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

Theorem pm4.71i 616
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 614 . 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  627  pm4.45  672  anabs1  786  2eu5  2197  imadmrn  4931  dff1o2  5334  map0e  6691  xpsnen  6831  dom0  6874  dfac5lem2  7635  pwfseqlem4  8164  axgroth6  8330  eqreznegel  10182  xrnemnf  10339  xrnepnf  10340  elioopnf  10615  elioomnf  10616  elicopnf  10617  elxrge0  10625  isprm2  12640  efgrelexlemb  14894  opsrtoslem1  16057  tgphaus  17631  ioombl1lem4  18750  vitalilem1  18795  ellogdm  19818  pjimai  22586  pm11.58  26755  bnj1101  27505
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