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

Theorem al2imi 1733
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 1732 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1715 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728
This theorem is referenced by:  alanimi  1734  alimdh  1735  albi  1736  aleximi  1749  19.33b  1802  aevlem0  1967  axc11nlemOLD2  1975  axc16g  2119  axc11rvOLD  2125  axc11nlemOLD  2146  axc11r  2175  axc10  2240  axc11nlemALT  2294  sbequi  2363  sbi1  2380  moim  2507  2eu6  2546  ral2imi  2931  ceqsalt  3201  difin0ss  3900  hbntg  30955  bj-2alim  31779  bj-ssbim  31810  bj-axc10v  31904  bj-ceqsalt0  32067  bj-ceqsalt1  32068  wl-spae  32485  wl-aetr  32496  wl-aleq  32501  wl-nfeqfb  32502  axc11-o  33254  pm10.57  37592  2al2imi  37594  19.41rg  37787  hbntal  37790
  Copyright terms: Public domain W3C validator