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	⊢ (φ → (ψ ↔ (ψ ∧ φ)))

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		pm3.21 435	. 2 ⊢ (φ → (ψ → (ψ ∧ φ)))
2		simpl 443	. 2 ⊢ ((ψ ∧ φ) → ψ)
3	1, 2	impbid1 194	1 ⊢ (φ → (ψ ↔ (ψ ∧ φ)))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  3505  dfphi2  4569  opres  4978  resieq  4979  cores  5084  fvres  5342  fressnfv  5439  epelcres  6328