Theorem iba 642

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 587	1 |- (ph -> (ps <-> (ps /\ ph)))

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

This theorem is referenced by:  pm5.54 683  biantru 724  dedlem0a 760  dedlema 762  unineq 2255  dmsnop 3328  fressnfv 3838  odi 4210  pw2en 4446  ltpiord 5015  ltmpi 5031  qsqueeze 6280  mdbr2 10223  mdsl2 10249

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