![]() |
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 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 2636 2eu6 2645 euind 3716 reuind 3745 sbnfc2 4438 opelopabt 5534 ssrel 5784 ssrelOLD 5785 ssrelrel 5798 fundif 6603 opabbrex 7471 fnoprabg 7543 tz7.48lem 8462 ssrelf 32484 bj-3exbi 36221 mpobi123f 37763 mptbi12f 37767 ismrc 42260 refimssco 43176 19.33-2 43958 pm11.63 43971 pm11.71 43973 axc5c4c711to11 43981 ichal 46940 |
Copyright terms: Public domain | W3C validator |