![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > al2imi | Structured version Visualization version Unicode version |
Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.) |
Ref | Expression |
---|---|
al2imi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
al2imi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | al2im 1686 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | al2imi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpg 1671 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1669 ax-4 1682 |
This theorem is referenced by: alanimi 1688 alimdh 1689 albi 1690 aleximi 1704 19.33b 1748 axc112 2020 axc11nlem 2021 axc10 2096 axc11nlemALT 2142 sbequi 2204 sbi1 2221 moim 2348 2eu6 2387 ral2imi 2776 ralimOLD 2782 ceqsalt 3070 difin0ss 3833 intssOLD 4256 hbntg 30452 bj-2alim 31202 bj-ssbim 31234 bj-axc10v 31318 bj-axc11nlemv 31347 bj-ceqsalt0 31482 bj-ceqsalt1 31483 wl-aetr 31863 wl-aleq 31868 wl-nfeqfb 31870 axc11-o 32522 pm10.57 36720 2al2imi 36722 19.41rg 36917 hbntal 36920 |
Copyright terms: Public domain | W3C validator |