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

Theorem al2imi 1731
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 1730 . 2 (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2 al2imi.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mpg 1713 1 (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1711  ax-4 1726
This theorem is referenced by:  alanimi  1732  alimdh  1733  albi  1734  aleximi  1747  19.33b  1800  aevlem0  1965  axc11nlemOLD2  1973  axc16g  2116  axc11rvOLD  2122  axc11nlemOLD  2141  axc11r  2169  axc10  2234  axc11nlemALT  2289  sbequi  2358  sbi1  2375  moim  2502  2eu6  2541  ral2imi  2926  ceqsalt  3196  difin0ss  3895  hbntg  30757  bj-2alim  31581  bj-ssbim  31612  bj-axc10v  31706  bj-ceqsalt0  31866  bj-ceqsalt1  31867  wl-spae  32284  wl-aetr  32295  wl-aleq  32300  wl-nfeqfb  32301  axc11-o  33053  pm10.57  37391  2al2imi  37393  19.41rg  37586  hbntal  37589
  Copyright terms: Public domain W3C validator