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

Step	Hyp	Ref	Expression
1		al2im 1808	. 2 ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
2		al2imi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	mpg 1791	1 ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

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  3075  ceqsalt  3496  elabgt  3653  elabgtOLD  3654  sstr2  3979  ssralv  4041  difin0ss  4364  axprlem2  5418  hbntg  35457  bj-2alim  36143  bj-cbvalimt  36171  bj-axc10v  36326  bj-sblem1  36375  bj-sblem2  36376  bj-ceqsalt0  36418  bj-ceqsalt1  36419  wl-spae  37044  wl-aetr  37052  wl-axc11r  37053  wl-aleq  37058  wl-nfeqfb  37059  axc11-o  38478  pm10.57  43872  2al2imi  43874  19.41rg  44053  hbntal  44056

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »