Theorem iba

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

	Ref	Expression
Assertion	iba	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜓 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.21	⊢ ( 𝜑 → ( 𝜓 → ( 𝜓 ∧ 𝜑 ) ) )
2		simpl	⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜓 )
3	1 2	impbid1	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜓 ∧ 𝜑 ) ) )