alanimi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > alanimi		Structured version Visualization version GIF version

Theorem alanimi 1810

Description: Variant of al2imi 1809 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)

**Hypothesis**
Ref	Expression
alanimi.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

**Assertion**
Ref	Expression
alanimi	⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)

**Proof of Theorem alanimi**
Step	Hyp	Ref	Expression
1		alanimi.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 411	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	al2imi 1809	. 2 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
4	3	imp 405	1 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∀wal 1531

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803

This theorem depends on definitions: df-bi 206 df-an 395

This theorem is referenced by: 19.26 1865 alsyl 1888 ax13 2368 nfeqf 2374 darapti 2672 axextmo 2700 vtoclgft 3530 euind 3716 reuind 3745 sbeqalb 3841 bm1.3ii 5303 trin2 6130 ssfi 9197 bj-nnfan 36340 bj-cbv3ta 36378 bj-bm1.3ii 36658 mpobi123f 37750 mptbi12f 37754 cotrintab 43156 albitr 43912 2alanimi 43921 ichan 46902

	
		OSZAR »