Metamath Proof Explorer


Theorem jca3

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010)

Ref Expression
Hypotheses jca3.1 ( 𝜑 → ( 𝜓𝜒 ) )
jca3.2 ( 𝜃𝜏 )
Assertion jca3 ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜒𝜏 ) ) ) )

Proof

Step Hyp Ref Expression
1 jca3.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 jca3.2 ( 𝜃𝜏 )
3 1 imp ( ( 𝜑𝜓 ) → 𝜒 )
4 3 a1d ( ( 𝜑𝜓 ) → ( 𝜃𝜒 ) )
5 4 2 jca2 ( ( 𝜑𝜓 ) → ( 𝜃 → ( 𝜒𝜏 ) ) )
6 5 ex ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜒𝜏 ) ) ) )