Metamath Proof Explorer


Theorem ecase3adOLD

Description: Obsolete version of ecase3ad as of 20-Sep-2024. (Contributed by NM, 24-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ecase3ad.1 ( 𝜑 → ( 𝜓𝜃 ) )
ecase3ad.2 ( 𝜑 → ( 𝜒𝜃 ) )
ecase3ad.3 ( 𝜑 → ( ( ¬ 𝜓 ∧ ¬ 𝜒 ) → 𝜃 ) )
Assertion ecase3adOLD ( 𝜑𝜃 )

Proof

Step Hyp Ref Expression
1 ecase3ad.1 ( 𝜑 → ( 𝜓𝜃 ) )
2 ecase3ad.2 ( 𝜑 → ( 𝜒𝜃 ) )
3 ecase3ad.3 ( 𝜑 → ( ( ¬ 𝜓 ∧ ¬ 𝜒 ) → 𝜃 ) )
4 notnotr ( ¬ ¬ 𝜓𝜓 )
5 4 1 syl5 ( 𝜑 → ( ¬ ¬ 𝜓𝜃 ) )
6 notnotr ( ¬ ¬ 𝜒𝜒 )
7 6 2 syl5 ( 𝜑 → ( ¬ ¬ 𝜒𝜃 ) )
8 5 7 3 ecased ( 𝜑𝜃 )