![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alimi | GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alimi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alimi | ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1404 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | |
2 | alimi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1408 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1310 |
This theorem was proved from axioms: ax-mp 7 ax-5 1404 ax-gen 1406 |
This theorem is referenced by: 2alimi 1413 al2imi 1415 alrimih 1426 hbal 1434 19.26 1438 19.33 1441 hbequid 1474 equidqe 1493 hbim 1505 hbor 1506 nford 1527 nfand 1528 nfalt 1538 19.21ht 1541 exbi 1564 19.29 1580 19.25 1586 alexim 1605 alexnim 1608 19.9hd 1621 19.32r 1639 ax10 1676 spimh 1696 equvini 1712 nfexd 1715 stdpc4 1729 ax10oe 1749 sbcof2 1762 sb4bor 1787 nfsb2or 1789 spsbim 1795 ax16i 1810 sbi2v 1844 nfsbt 1923 nfsbd 1924 sbalyz 1948 hbsb4t 1962 dvelimor 1967 sbal2 1971 mo2n 2001 eumo0 2004 mor 2015 bm1.1 2098 alral 2450 rgen2a 2458 ralimi2 2464 rexim 2498 r19.32r 2550 ceqsalt 2681 spcgft 2732 spcegft 2734 spc2gv 2745 spc3gv 2747 rspct 2751 elabgt 2793 reu6 2840 sbciegft 2905 csbnestgf 3016 ssrmof 3124 rabss2 3144 rabxmdc 3358 undif4 3389 ssdif0im 3391 inssdif0im 3394 ssundifim 3410 ralf0 3430 ralm 3431 intmin4 3763 dfiin2g 3810 invdisj 3887 trint 3999 a9evsep 4008 axnul 4011 csbexga 4014 exmidn0m 4082 exmidsssn 4083 exmidsssnc 4084 exmid0el 4085 ordunisuc2r 4388 tfi 4454 peano5 4470 ssrelrel 4597 issref 4877 iotanul 5059 iota4 5062 dffun5r 5091 fv3 5396 mptfvex 5458 ssoprab2 5779 mpofvex 6053 tfri1dALT 6200 bj-nfalt 12655 elabgft1 12668 bj-rspgt 12676 bj-axemptylem 12773 bj-indind 12813 setindis 12848 bdsetindis 12850 bj-inf2vnlem1 12851 bj-inf2vn 12855 bj-inf2vn2 12856 |
Copyright terms: Public domain | W3C validator |