Theorem ancrb

Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Conclusion

\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \psi \wedge \varphi \)

Proof

iba

pm5.74i _