![]() |
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 1808 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓) |
3 | 2 | alimi 1808 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1792 ax-4 1806 |
This theorem is referenced by: alcomimw 2040 2mo 2646 2eu6 2655 euind 3733 reuind 3762 sbnfc2 4445 opelopabt 5542 ssrel 5795 ssrelOLD 5796 ssrelrel 5809 fundif 6617 opabbrex 7484 fnoprabg 7556 tz7.48lem 8480 ssrelf 32635 bj-3exbi 36599 mpobi123f 38149 mptbi12f 38153 ismrc 42689 refimssco 43597 19.33-2 44378 pm11.63 44391 pm11.71 44393 axc5c4c711to11 44401 ichal 47391 |
Copyright terms: Public domain | W3C validator |