Theorem alrimih 1821

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nexdh  1863  albidh  1864  alrimiv  1925  ax12i  1964  cbvaliw  2003  nf5dh  2145  alrimi  2211  hbnd  2295  cbv3v  2336  cbv3  2400  eujustALT  2570  axi5r  2698  hbralrimi  3142  ralidmw  4514  bnj1093  34973  bj-abvALT  36890  bj-gabssd  36919  mpobi123f  38149  axc4i-o  38880  equidq  38906  aev-o  38913  ax12f  38922  axc5c4c711  44397  hbimpg  44552  gen11nv  44615