Metamath Proof Explorer


Theorem 3jaodd

Description: Double deduction form of 3jaoi . (Contributed by Scott Fenton, 20-Apr-2011)

Ref Expression
Hypotheses 3jaodd.1 ( 𝜑 → ( 𝜓 → ( 𝜒𝜂 ) ) )
3jaodd.2 ( 𝜑 → ( 𝜓 → ( 𝜃𝜂 ) ) )
3jaodd.3 ( 𝜑 → ( 𝜓 → ( 𝜏𝜂 ) ) )
Assertion 3jaodd ( 𝜑 → ( 𝜓 → ( ( 𝜒𝜃𝜏 ) → 𝜂 ) ) )

Proof

Step Hyp Ref Expression
1 3jaodd.1 ( 𝜑 → ( 𝜓 → ( 𝜒𝜂 ) ) )
2 3jaodd.2 ( 𝜑 → ( 𝜓 → ( 𝜃𝜂 ) ) )
3 3jaodd.3 ( 𝜑 → ( 𝜓 → ( 𝜏𝜂 ) ) )
4 1 com3r ( 𝜒 → ( 𝜑 → ( 𝜓𝜂 ) ) )
5 2 com3r ( 𝜃 → ( 𝜑 → ( 𝜓𝜂 ) ) )
6 3 com3r ( 𝜏 → ( 𝜑 → ( 𝜓𝜂 ) ) )
7 4 5 6 3jaoi ( ( 𝜒𝜃𝜏 ) → ( 𝜑 → ( 𝜓𝜂 ) ) )
8 7 com3l ( 𝜑 → ( 𝜓 → ( ( 𝜒𝜃𝜏 ) → 𝜂 ) ) )