Metamath Proof Explorer


Theorem ecase2dOLD

Description: Obsolete version of ecase2d as of 19-Sep-2024. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Dec-2012) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ecase2d.1
|- ( ph -> ps )
ecase2d.2
|- ( ph -> -. ( ps /\ ch ) )
ecase2d.3
|- ( ph -> -. ( ps /\ th ) )
ecase2d.4
|- ( ph -> ( ta \/ ( ch \/ th ) ) )
Assertion ecase2dOLD
|- ( ph -> ta )

Proof

Step Hyp Ref Expression
1 ecase2d.1
 |-  ( ph -> ps )
2 ecase2d.2
 |-  ( ph -> -. ( ps /\ ch ) )
3 ecase2d.3
 |-  ( ph -> -. ( ps /\ th ) )
4 ecase2d.4
 |-  ( ph -> ( ta \/ ( ch \/ th ) ) )
5 idd
 |-  ( ph -> ( ta -> ta ) )
6 2 pm2.21d
 |-  ( ph -> ( ( ps /\ ch ) -> ta ) )
7 1 6 mpand
 |-  ( ph -> ( ch -> ta ) )
8 3 pm2.21d
 |-  ( ph -> ( ( ps /\ th ) -> ta ) )
9 1 8 mpand
 |-  ( ph -> ( th -> ta ) )
10 7 9 jaod
 |-  ( ph -> ( ( ch \/ th ) -> ta ) )
11 5 10 4 mpjaod
 |-  ( ph -> ta )