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 1732 | . 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) | |
2 | al2imi.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | mpg 1715 | 1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1713 ax-4 1728 |
This theorem is referenced by: alanimi 1734 alimdh 1735 albi 1736 aleximi 1749 19.33b 1802 aevlem0 1967 axc11nlemOLD2 1975 axc16g 2119 axc11rvOLD 2125 axc11nlemOLD 2146 axc11r 2175 axc10 2240 axc11nlemALT 2294 sbequi 2363 sbi1 2380 moim 2507 2eu6 2546 ral2imi 2931 ceqsalt 3201 difin0ss 3900 hbntg 30955 bj-2alim 31779 bj-ssbim 31810 bj-axc10v 31904 bj-ceqsalt0 32067 bj-ceqsalt1 32068 wl-spae 32485 wl-aetr 32496 wl-aleq 32501 wl-nfeqfb 32502 axc11-o 33254 pm10.57 37592 2al2imi 37594 19.41rg 37787 hbntal 37790 |
Copyright terms: Public domain | W3C validator |