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  2200  imadmrn  4998  dff1o2  5401  map0e  6759  xpsnen  6900  dom0  6943  dfac5lem2  7705  pwfseqlem4  8238  axgroth6  8404  eqreznegel  10256  xrnemnf  10413  xrnepnf  10414  elioopnf  10689  elioomnf  10690  elicopnf  10691  elxrge0  10699  isprm2  12714  efgrelexlemb  15007  opsrtoslem1  16173  tgphaus  17747  ioombl1lem4  18866  vitalilem1  18911  ellogdm  19934  pjimai  22702  pm11.58  26942  bnj1101  27849
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