2alimi - Metamath Proof Explorer

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

Theorem 2alimi 1806

Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

**Hypothesis**
Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

**Assertion**
Ref	Expression
2alimi	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)

**Proof of Theorem 2alimi**
Step	Hyp	Ref	Expression
1		alimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	alimi 1805	. 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓)
3	2	alimi 1805	1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∀wal 1531

This theorem was proved from axioms: ax-mp 5 ax-gen 1789 ax-4 1803

This theorem is referenced by: alcomiw 2038 2mo 2639 2eu6 2648 euind 3721 reuind 3750 sbnfc2 4440 opelopabt 5538 ssrel 5788 ssrelOLD 5789 ssrelrel 5802 fundif 6607 opabbrex 7477 fnoprabg 7549 tz7.48lem 8468 ssrelf 32426 bj-3exbi 36126 mpobi123f 37668 mptbi12f 37672 ismrc 42152 refimssco 43068 19.33-2 43850 pm11.63 43863 pm11.71 43865 axc5c4c711to11 43873 ichal 46835

	
		OSZAR »