alcoms - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > alcoms		Unicode version

Theorem alcoms 1843

Description: Swap quantifiers in an antecedent. (Contributed by NM, 11-May-1993.)

**Hypothesis**
Ref	Expression
alcoms.1

**Assertion**
Ref	Expression
alcoms

**Proof of Theorem alcoms**
Step	Hyp	Ref	Expression
1		ax-11 1842	. 2
2		alcoms.1	. 2
3	1, 2	syl 16	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 A.wal 1393

This theorem is referenced by: cbv3hv 1956 cbv2h 2019 axc11n-16 2268 mo3 2323 mo3OLD 2324 wl-equsal1i 29996 wl-mo3t 30021 axc11next 31313 bj-nfalt 34265 bj-cbv3ta 34270 bj-cbv2hv 34294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-11 1842