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 1803 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓) |
3 | 2 | alimi 1803 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1787 ax-4 1801 |
This theorem is referenced by: alcomiw 2041 alcomiwOLD 2042 2mo 2726 2eu6 2737 euind 3712 reuind 3741 sbnfc2 4385 opelopabt 5410 ssrel 5650 ssrelrel 5662 fundif 6396 opabbrex 7196 fnoprabg 7264 tz7.48lem 8066 ssrelf 30294 bj-3exbi 33847 mpobi123f 35321 mptbi12f 35325 ismrc 39176 refimssco 39845 19.33-2 40591 pm11.63 40604 pm11.71 40606 axc5c4c711to11 40614 ichal 43504 ichan 43507 |
Copyright terms: Public domain | W3C validator |