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

Theorem al2imi 1900
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 1899 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1879 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1877  ax-4 1894
This theorem is referenced by:  alanimi  1901  alimdh  1902  albi  1903  aleximi  1916  19.33b  1975  aevlem0  2149  axc16g  2313  axc11rvOLD  2319  axc11r  2363  axc10  2428  sbequi  2536  sbi1  2553  moim  2693  2eu6  2733  ral2imi  3146  ceqsalt  3433  difin0ss  4158  hbntg  32052  bj-2alim  32930  bj-ssbim  32958  bj-axc10v  33053  bj-ceqsalt0  33199  bj-ceqsalt1  33200  wl-spae  33640  wl-aetr  33649  wl-aleq  33654  wl-nfeqfb  33655  axc11-o  34748  pm10.57  39087  2al2imi  39089  19.41rg  39281  hbntal  39284
  Copyright terms: Public domain W3C validator