|   | 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 1813 | . 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) | |
| 2 | al2imi.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 3 | 1, 2 | mpg 1796 | 1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1794 ax-4 1808 | 
| This theorem is referenced by: alanimi 1815 alimdh 1816 albi 1817 aleximi 1831 19.33b 1884 aevlem0 2053 sbi1 2070 axc16g 2259 axc11r 2370 axc10 2389 axc15 2426 sb2 2483 moim 2543 2eu6 2656 ral2imi 3084 ceqsalt 3514 spcimgft 3545 elabgt 3671 elabgtOLD 3672 sstr2 3989 ssralv 4051 difin0ss 4372 sepexlem 5298 axprlem2 5423 axnulg 35107 hbntg 35807 bj-2alim 36612 bj-cbvalimt 36641 bj-axc10v 36795 bj-sblem1 36844 bj-sblem2 36845 bj-ceqsalt0 36886 bj-ceqsalt1 36887 wl-spae 37523 wl-aetr 37531 wl-axc11r 37532 wl-aleq 37537 wl-nfeqfb 37538 axc11-o 38953 pm10.57 44395 2al2imi 44397 19.41rg 44575 hbntal 44578 | 
| Copyright terms: Public domain | W3C validator |