Metamath Proof Explorer


Theorem 3anim2i

Description: Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019)

Ref Expression
Hypothesis 3animi.1 ( 𝜑𝜓 )
Assertion 3anim2i ( ( 𝜒𝜑𝜃 ) → ( 𝜒𝜓𝜃 ) )

Proof

Step Hyp Ref Expression
1 3animi.1 ( 𝜑𝜓 )
2 id ( 𝜒𝜒 )
3 id ( 𝜃𝜃 )
4 2 1 3 3anim123i ( ( 𝜒𝜑𝜃 ) → ( 𝜒𝜓𝜃 ) )