Description: Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | anbi1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | 1 | anbi1d | |