Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  al2imi Structured version   Visualization version   GIF version

Theorem al2imi 1740
 Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
al2imi.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
al2imi (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Proof of Theorem al2imi
StepHypRef Expression
1 al2im 1739 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1721 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1478 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1719  ax-4 1734 This theorem is referenced by:  alanimi  1741  alimdh  1742  albi  1743  aleximi  1756  19.33b  1810  aevlem0  1977  axc11nlemOLD2  1985  axc16g  2130  axc11rvOLD  2136  axc11nlemOLD  2157  axc11r  2186  axc10  2251  axc11nlemALT  2305  sbequi  2374  sbi1  2391  moim  2518  2eu6  2557  ral2imi  2943  ceqsalt  3218  difin0ss  3926  hbntg  31465  bj-2alim  32289  bj-ssbim  32316  bj-axc10v  32412  bj-ceqsalt0  32573  bj-ceqsalt1  32574  wl-spae  32977  wl-aetr  32988  wl-aleq  32993  wl-nfeqfb  32994  axc11-o  33755  pm10.57  38091  2al2imi  38093  19.41rg  38287  hbntal  38290
 Copyright terms: Public domain W3C validator