Theorem ibar 490

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)

Assertion

Ref	Expression
ibar	⊢ (φ → (ψ ↔ (φ ∧ ψ)))

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 434	. 2 ⊢ (φ → (ψ → (φ ∧ ψ)))
2		simpr 447	. 2 ⊢ ((φ ∧ ψ) → ψ)
3	1, 2	impbid1 194	1 ⊢ (φ → (ψ ↔ (φ ∧ ψ)))

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:  biantrur  492  biantrurd  494  anclb  530  pm5.42  531  anabs5  784  pm5.33  848  bianabs  850  baib  871  baibd  875  pclem6  896  cad1  1398  euan  2261  eueq3  3011  ifan  3701  lefinlteq  4463  fvopab3g  5386