Theorem iba 489

Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)

Assertion

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

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		pm3.21 435	. 2 |- (ph -> (ps -> (ps /\ ph)))
2		simpl 443	. 2 |- ((ps /\ ph) -> ps)
3	1, 2	impbid1 194	1 |- (ph -> (ps <-> (ps /\ ph)))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  biantru  491  biantrud  493  ancrb  533  pm5.54  870  rbaibd  876  dedlem0a  918  unineq  3506  dfphi2  4570  opres  4979  resieq  4980  cores  5085  fvres  5343  fressnfv  5440  epelcres  6329