![]() |
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 1447 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | |
2 | alimi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1451 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 |
This theorem was proved from axioms: ax-mp 5 ax-5 1447 ax-gen 1449 |
This theorem is referenced by: 2alimi 1456 al2imi 1458 alrimih 1469 hbal 1477 19.26 1481 19.33 1484 hbequid 1513 equidqe 1532 hbim 1545 hbor 1546 nford 1567 nfand 1568 nfal 1576 nfalt 1578 19.21ht 1581 exbi 1604 19.29 1620 19.25 1626 alexim 1645 alexnim 1648 19.9hd 1662 19.32r 1680 ax10 1717 spimh 1737 equvini 1758 nfexd 1761 stdpc4 1775 ax10oe 1797 sbcof2 1810 sb4bor 1835 nfsb2or 1837 spsbim 1843 ax16i 1858 sbi2v 1892 nfsbt 1976 nfsbd 1977 sbalyz 1999 hbsb4t 2013 dvelimor 2018 sbal2 2020 mo2n 2054 eumo0 2057 mor 2068 bm1.1 2162 alral 2522 rgen2a 2531 ralimi2 2537 rexim 2571 r19.32r 2623 ceqsalt 2763 spcgft 2814 spcegft 2816 spc2gv 2828 spc3gv 2830 rspct 2834 elabgt 2878 reu6 2926 sbciegft 2993 csbeq2 3081 csbnestgf 3109 ssrmof 3218 rabss2 3238 rabxmdc 3454 undif4 3485 ssdif0im 3487 inssdif0im 3490 ssundifim 3506 ralf0 3526 ralm 3527 intmin4 3872 dfiin2g 3919 invdisj 3997 trint 4116 a9evsep 4125 axnul 4128 csbexga 4131 exmidn0m 4201 exmidsssn 4202 exmidsssnc 4203 exmid0el 4204 ordunisuc2r 4513 tfi 4581 peano5 4597 ssrelrel 4726 issref 5011 iotanul 5193 iota4 5196 dffun5r 5228 fv3 5538 mptfvex 5601 ssoprab2 5930 mpofvex 6203 tfri1dALT 6351 prodeq2w 11559 bj-nfalt 14398 elabgft1 14412 bj-rspgt 14420 bj-axemptylem 14526 bj-indind 14566 setindis 14601 bdsetindis 14603 bj-inf2vnlem1 14604 bj-inf2vn 14608 bj-inf2vn2 14609 |
Copyright terms: Public domain | W3C validator |