Theorem alrimih 1856

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2246 and 19.21h 2323. Instance of sylg 1855. (Contributed by NM, 9-Jan-1993.)

Hypotheses

Ref	Expression
alrimih.1	⊢ (𝜑 → ∀𝑥𝜑)
alrimih.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimih	⊢ (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimih

Step	Hyp	Ref	Expression
1		alrimih.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimih.2	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	sylg 1855	1 ⊢ (𝜑 → ∀𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841

This theorem is used by:  nexdh  1897  albidh  1898  alrimiv  1961  ax12i  2000  cbvaliw  2040  nf5dh  2186  nfexhe  2213  alrimi  2252  hbnd  2332  cbv3v  2367  cbv3  2429  eujustALT  2600  axi5r  2727  hbralrimi  3156  ralidmw  4475  bnj1093  35666  bj-abvALT  37952  bj-gabssd  37982  mpobi123f  39240  axc4i-o  40101  equidq  40127  aev-o  40134  ax12f  40143  axc5c4c711  45531  hbimpg  45682  gen11nv  45745