Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of WhiteheadRussell p. 120. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 2-Dec-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | pm4.71 | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 ↔ ( 𝜑 ∧ 𝜓 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) | |
2 | 1 | biantru | ⊢ ( ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ) ) |
3 | anclb | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ) | |
4 | dfbi2 | ⊢ ( ( 𝜑 ↔ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ) ) | |
5 | 2 3 4 | 3bitr4i | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 ↔ ( 𝜑 ∧ 𝜓 ) ) ) |