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

Theorem al2imi 1809
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 1808 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1791 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1789  ax-4 1803
This theorem is referenced by:  alanimi  1810  alimdh  1811  albi  1812  aleximi  1826  19.33b  1880  aevlem0  2049  sbi1  2066  axc16g  2246  axc11r  2359  axc10  2378  axc15  2415  sb2  2472  moim  2532  2eu6  2645  ral2imi  3074  ceqsalt  3494  elabgt  3657  elabgtOLD  3658  sstr2  3983  ssralv  4045  difin0ss  4370  axprlem2  5424  hbntg  35529  bj-2alim  36215  bj-cbvalimt  36243  bj-axc10v  36398  bj-sblem1  36447  bj-sblem2  36448  bj-ceqsalt0  36490  bj-ceqsalt1  36491  wl-spae  37116  wl-aetr  37124  wl-axc11r  37125  wl-aleq  37130  wl-nfeqfb  37131  axc11-o  38550  pm10.57  43947  2al2imi  43949  19.41rg  44128  hbntal  44131
  Copyright terms: Public domain W3C validator