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

Theorem al2imi 1817
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 1816 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1799 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811
This theorem is referenced by:  alanimi  1818  alimdh  1819  albi  1820  aleximi  1833  19.33b  1887  aevlem0  2060  sbi1  2077  axc16g  2263  sbi1vOLD  2325  axc11r  2388  axc10  2405  axc15  2446  sb2  2506  sbequiOLD  2536  sbi1OLD  2544  sbequiALT  2598  sbi1ALT  2608  moim  2628  2eu6  2745  ral2imi  3151  ceqsalt  3513  difin0ss  4311  axprlem2  5312  hbntg  33107  bj-2alim  34001  bj-cbvalimt  34029  bj-axc10v  34174  bj-sblem1  34225  bj-sblem2  34226  bj-ceqsalt0  34268  bj-ceqsalt1  34269  wl-spae  34871  wl-aetr  34879  wl-axc11r  34880  wl-aleq  34885  wl-nfeqfb  34886  axc11-o  36192  pm10.57  40995  2al2imi  40997  19.41rg  41176  hbntal  41179
  Copyright terms: Public domain W3C validator