Metamath Proof Explorer


Theorem anim12

Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d . Theorem *3.47 of WhiteheadRussell p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993) (Proof shortened by Wolf Lammen, 7-Apr-2013)

Ref Expression
Assertion anim12 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) → ( ( 𝜑𝜒 ) → ( 𝜓𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 id ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )
2 id ( ( 𝜒𝜃 ) → ( 𝜒𝜃 ) )
3 1 2 im2anan9 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) → ( ( 𝜑𝜒 ) → ( 𝜓𝜃 ) ) )