Description: Conjoin antecedent to left of consequent. Theorem *4.7 of WhiteheadRussell p. 120. (Contributed by NM, 25-Jul-1999) (Proof shortened by Wolf Lammen, 24-Mar-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | anclb | |- ( ( ph -> ps ) <-> ( ph -> ( ph /\ ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ibar | |- ( ph -> ( ps <-> ( ph /\ ps ) ) ) |
|
| 2 | 1 | pm5.74i | |- ( ( ph -> ps ) <-> ( ph -> ( ph /\ ps ) ) ) |