Theorem alrimih 1751

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2075 and 19.21h 2121. Instance of sylg 1750. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.)

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 1750	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1481

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

This theorem is referenced by:  nexdh  1792  albidh  1793  alrimiv  1855  ax12i  1879  cbvaliw  1933  nf5dh  2026  alrimi  2082  hbnd  2147  alrimiOLD  2192  cbvalv  2273  aevALTOLD  2321  eujustALT  2473  axi5r  2594  hbralrimi  2954  bnj1093  31048  bj-abv  32901  bj-ab0  32902  mpt2bi123f  33971  axc4i-o  34183  equidq  34209  aev-o  34216  ax12f  34225  axc5c4c711  38602  hbimpg  38770  gen11nv  38842