![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 2alimi | Structured version Unicode 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 1605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | alimi 1605 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-gen 1592 ax-4 1603 |
This theorem is referenced by: mo3OLD 2305 moOLD 2311 2mo 2366 2moOLD 2367 2moOLDOLD 2368 2eu6 2377 2eu6OLD 2378 euind 3229 reuind 3246 sbnfc2 3790 opelopabt 4685 ssrel 5012 ssrelrel 5024 fnoprabg 6277 tz7.48lem 6982 ssrelf 26065 mpt2bi123f 29099 mptbi12f 29103 ismrc 29161 19.33-2 29758 pm11.63 29772 pm11.71 29774 axc5c4c711to11 29783 bj-3exbi 32430 |
Copyright terms: Public domain | W3C validator |