![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > al2imi | Structured version Visualization version GIF 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 1808 | . 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) | |
2 | al2imi.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | mpg 1791 | 1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1789 ax-4 1803 |
This theorem is referenced by: alanimi 1810 alimdh 1811 albi 1812 aleximi 1826 19.33b 1880 aevlem0 2049 sbi1 2066 axc16g 2246 axc11r 2359 axc10 2378 axc15 2415 sb2 2472 moim 2532 2eu6 2645 ral2imi 3074 ceqsalt 3494 elabgt 3657 elabgtOLD 3658 sstr2 3983 ssralv 4045 difin0ss 4370 axprlem2 5424 hbntg 35529 bj-2alim 36215 bj-cbvalimt 36243 bj-axc10v 36398 bj-sblem1 36447 bj-sblem2 36448 bj-ceqsalt0 36490 bj-ceqsalt1 36491 wl-spae 37116 wl-aetr 37124 wl-axc11r 37125 wl-aleq 37130 wl-nfeqfb 37131 axc11-o 38550 pm10.57 43947 2al2imi 43949 19.41rg 44128 hbntal 44131 |
Copyright terms: Public domain | W3C validator |