This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4cases

Description: Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003)

	Ref	Expression
Hypotheses	4cases.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
	4cases.2	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 )
	4cases.3	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) → 𝜒 )
	4cases.4	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜒 )
Assertion	4cases	⊢ 𝜒

Proof

Step	Hyp	Ref	Expression
1		4cases.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		4cases.2	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 )
3		4cases.3	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) → 𝜒 )
4		4cases.4	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜒 )
5	1 3	pm2.61ian	⊢ ( 𝜓 → 𝜒 )
6	2 4	pm2.61ian	⊢ ( ¬ 𝜓 → 𝜒 )
7	5 6	pm2.61i	⊢ 𝜒