Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2alimi | Structured version Visualization version GIF version |
Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Ref | Expression |
---|---|
alimi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2alimi | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alimi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alimi 1806 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓) |
3 | 2 | alimi 1806 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1529 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1790 ax-4 1804 |
This theorem is referenced by: alcomiw 2044 alcomiwOLD 2045 2mo 2727 2eu6 2738 euind 3713 reuind 3742 sbnfc2 4386 opelopabt 5410 ssrel 5650 ssrelrel 5662 fundif 6396 opabbrex 7199 fnoprabg 7267 tz7.48lem 8069 ssrelf 30358 bj-3exbi 33943 mpobi123f 35432 mptbi12f 35436 ismrc 39289 refimssco 39958 19.33-2 40705 pm11.63 40718 pm11.71 40720 axc5c4c711to11 40728 ichal 43618 ichan 43621 |
Copyright terms: Public domain | W3C validator |