Metamath Proof Explorer
Description: Ordering elimination by cases. (Contributed by NM, 6Jul2007)


Ref 
Expression 

Hypotheses 
lecase.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) 


lecase.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 


lecase.3 
⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝜓 ) 


lecase.4 
⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝜓 ) 

Assertion 
lecasei 
⊢ ( 𝜑 → 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

lecase.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) 
2 

lecase.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 
3 

lecase.3 
⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝜓 ) 
4 

lecase.4 
⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝜓 ) 
5 

letric 
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) ) 
6 
1 2 5

syl2anc 
⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) ) 
7 
3 4 6

mpjaodan 
⊢ ( 𝜑 → 𝜓 ) 