|   | 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 1810 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓) | 
| 3 | 2 | alimi 1810 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 | 
| This theorem was proved from axioms: ax-mp 5 ax-gen 1794 ax-4 1808 | 
| This theorem is referenced by: alcomimw 2041 2mo 2647 2eu6 2656 euind 3729 reuind 3758 sbnfc2 4438 opelopabt 5536 ssrel 5791 ssrelOLD 5792 ssrelrel 5805 fundif 6614 opabbrex 7485 fnoprabg 7557 tz7.48lem 8482 ssrelf 32628 bj-3exbi 36618 mpobi123f 38170 mptbi12f 38174 ismrc 42717 refimssco 43625 19.33-2 44406 pm11.63 44419 pm11.71 44421 axc5c4c711to11 44429 ichal 47458 | 
| Copyright terms: Public domain | W3C validator |