Theorem alrimih 1826

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2215 and 19.21h 2294. Instance of sylg 1825. (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 1825	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811

This theorem is referenced by:  nexdh  1867  albidh  1868  alrimiv  1929  ax12i  1968  cbvaliw  2008  nf5dh  2153  nfexhe  2183  alrimi  2221  hbnd  2303  cbv3v  2339  cbv3  2401  eujustALT  2572  axi5r  2700  hbralrimi  3127  ralidmw  4456  bnj1093  35122  bj-abvALT  37214  bj-gabssd  37243  mpobi123f  38483  axc4i-o  39344  equidq  39370  aev-o  39377  ax12f  39386  axc5c4c711  44828  hbimpg  44981  gen11nv  45044