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

Theorem al2imi 1783
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 1782 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1764 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1762  ax-4 1777
This theorem is referenced by:  alanimi  1784  alimdh  1785  albi  1786  aleximi  1799  19.33b  1853  aevlem0  2022  axc16g  2172  axc11rvOLD  2178  axc11r  2223  axc10  2288  sbequi  2403  sbi1  2420  moim  2548  2eu6  2587  ral2imi  2976  ceqsalt  3259  difin0ss  3979  hbntg  31835  bj-2alim  32719  bj-ssbim  32746  bj-axc10v  32842  bj-ceqsalt0  32998  bj-ceqsalt1  32999  wl-spae  33436  wl-aetr  33447  wl-aleq  33452  wl-nfeqfb  33453  axc11-o  34555  pm10.57  38887  2al2imi  38889  19.41rg  39083  hbntal  39086
  Copyright terms: Public domain W3C validator