Theorem alrimih 1825

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  nexdh  1866  albidh  1867  alrimiv  1928  ax12i  1967  cbvaliw  2007  nf5dh  2152  alrimi  2218  hbnd  2300  cbv3v  2337  cbv3  2399  eujustALT  2570  axi5r  2698  hbralrimi  3124  ralidmw  4467  bnj1093  35085  bj-abvALT  37051  bj-gabssd  37080  mpobi123f  38302  axc4i-o  39097  equidq  39123  aev-o  39130  ax12f  39139  nfexhe  42407  axc5c4c711  44584  hbimpg  44737  gen11nv  44800