![]() |
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 1458 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | |
2 | alimi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1462 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-5 1458 ax-gen 1460 |
This theorem is referenced by: 2alimi 1467 al2imi 1469 alrimih 1480 hbal 1488 19.26 1492 19.33 1495 hbequid 1524 equidqe 1543 hbim 1556 hbor 1557 nford 1578 nfand 1579 nfal 1587 nfalt 1589 19.21ht 1592 exbi 1615 19.29 1631 19.25 1637 alexim 1656 alexnim 1659 19.9hd 1673 19.32r 1691 ax10 1728 spimh 1748 equvini 1769 nfexd 1772 stdpc4 1786 ax10oe 1808 sbcof2 1821 sb4bor 1846 nfsb2or 1848 spsbim 1854 ax16i 1869 sbi2v 1904 nfsbt 1988 nfsbd 1989 sbalyz 2011 hbsb4t 2025 dvelimor 2030 sbal2 2032 mo2n 2066 eumo0 2069 mor 2080 bm1.1 2174 alral 2535 rgen2a 2544 ralimi2 2550 rexim 2584 r19.32r 2636 ceqsalt 2778 spcgft 2829 spcegft 2831 spc2gv 2843 spc3gv 2845 rspct 2849 elabgt 2893 reu6 2941 sbciegft 3008 csbeq2 3096 csbnestgf 3124 ssrmof 3233 rabss2 3253 rabxmdc 3469 undif4 3500 ssdif0im 3502 inssdif0im 3505 ssundifim 3521 ralf0 3541 ralm 3542 intmin4 3887 dfiin2g 3934 invdisj 4012 trint 4131 a9evsep 4140 axnul 4143 csbexga 4146 exmidn0m 4219 exmidsssn 4220 exmidsssnc 4221 exmid0el 4222 ordunisuc2r 4531 tfi 4599 peano5 4615 ssrelrel 4744 issref 5029 iotanul 5211 iota4 5215 dffun5r 5247 fv3 5557 mptfvex 5622 ssoprab2 5953 mpofvex 6229 tfri1dALT 6377 prodeq2w 11599 bj-nfalt 14994 elabgft1 15008 bj-rspgt 15016 bj-axemptylem 15122 bj-indind 15162 setindis 15197 bdsetindis 15199 bj-inf2vnlem1 15200 bj-inf2vn 15204 bj-inf2vn2 15205 |
Copyright terms: Public domain | W3C validator |