Theorem iba 704

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 357	. 2 |- ((ph -> ps) <-> (ph -> (ps /\ ph)))
2	1	pm5.74ri 647	1 |- (ph -> (ps <-> (ps /\ ph)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm5.54 747  biantru 793  dedlem0aOLD 835  dedlemaOLD 838  unineq 2844  dmsnopOLD 4368  cores 4400  fressnfv 4813  odi 5258  pw2en 5505  ltpiord 6167  ltmpi 6183  qsqueeze 7461  mdbr2 11868  mdsl2i 11894

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 164  df-an 242

Copyright terms: Public domain