Theorem iba 644

Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121.

Assertion

Ref	Expression
iba	|- (ph -> (ps <-> (ps /\ ph)))

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		ancrb 330	. 2 |- ((ph -> ps) <-> (ph -> (ps /\ ph)))
2	1	pm5.74ri 589	1 |- (ph -> (ps <-> (ps /\ ph)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm5.54 685  biantru 726  dedlem0a 762  dedlema 764  unineq 2258  dmsnop 3334  fressnfv 3844  odi 4216  pw2en 4452  ltpiord 5027  ltmpi 5043  qsqueeze 6281  mdbr2 10218  mdsl2 10244

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 147  df-an 225

Copyright terms: Public domain