Theorem pm4.71i 696

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120.

Hypothesis

Ref	Expression
pm4.71i.1	|- (ph -> ps)

Assertion

Ref	Expression
pm4.71i	|- (ph <-> (ph /\ ps))

Proof of Theorem pm4.71i

Step	Hyp	Ref	Expression
1		pm4.71i.1	. 2 |- (ph -> ps)
2		pm4.71 694	. 2 |- ((ph -> ps) <-> (ph <-> (ph /\ ps)))
3	1, 2	mpbi 205	1 |- (ph <-> (ph /\ ps))

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239

This theorem is referenced by:  pm4.45 699  2eu5 1694  imadmrn 4088  dff1o2 4450  map0e 5212  xpsnen 5305  aceq5lem2 5694  infmap2lem1 8643  dfms2 8871  axgroth6 9932  pjimai 11540  bnj142 12266  bnj1061 12690  bnj1101 12710  eqreznegel 13446  lbzbi 13449  isprm2 13567

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163  df-an 241

Copyright terms: Public domain