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 1434 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | |
2 | alimi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1438 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 |
This theorem was proved from axioms: ax-mp 5 ax-5 1434 ax-gen 1436 |
This theorem is referenced by: 2alimi 1443 al2imi 1445 alrimih 1456 hbal 1464 19.26 1468 19.33 1471 hbequid 1500 equidqe 1519 hbim 1532 hbor 1533 nford 1554 nfand 1555 nfal 1563 nfalt 1565 19.21ht 1568 exbi 1591 19.29 1607 19.25 1613 alexim 1632 alexnim 1635 19.9hd 1649 19.32r 1667 ax10 1704 spimh 1724 equvini 1745 nfexd 1748 stdpc4 1762 ax10oe 1784 sbcof2 1797 sb4bor 1822 nfsb2or 1824 spsbim 1830 ax16i 1845 sbi2v 1879 nfsbt 1963 nfsbd 1964 sbalyz 1986 hbsb4t 2000 dvelimor 2005 sbal2 2007 mo2n 2041 eumo0 2044 mor 2055 bm1.1 2149 alral 2509 rgen2a 2518 ralimi2 2524 rexim 2558 r19.32r 2610 ceqsalt 2747 spcgft 2798 spcegft 2800 spc2gv 2812 spc3gv 2814 rspct 2818 elabgt 2862 reu6 2910 sbciegft 2976 csbeq2 3064 csbnestgf 3092 ssrmof 3200 rabss2 3220 rabxmdc 3435 undif4 3466 ssdif0im 3468 inssdif0im 3471 ssundifim 3487 ralf0 3507 ralm 3508 intmin4 3846 dfiin2g 3893 invdisj 3970 trint 4089 a9evsep 4098 axnul 4101 csbexga 4104 exmidn0m 4174 exmidsssn 4175 exmidsssnc 4176 exmid0el 4177 ordunisuc2r 4485 tfi 4553 peano5 4569 ssrelrel 4698 issref 4980 iotanul 5162 iota4 5165 dffun5r 5194 fv3 5503 mptfvex 5565 ssoprab2 5889 mpofvex 6163 tfri1dALT 6310 prodeq2w 11483 bj-nfalt 13486 elabgft1 13500 bj-rspgt 13508 bj-axemptylem 13615 bj-indind 13655 setindis 13690 bdsetindis 13692 bj-inf2vnlem1 13693 bj-inf2vn 13697 bj-inf2vn2 13698 |
Copyright terms: Public domain | W3C validator |