Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  alrimih Structured version   Visualization version   GIF version

Theorem alrimih 1749
 Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2073 and 19.21h 2119. Instance of sylg 1748. (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
StepHypRef Expression
1 alrimih.1 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimih.2 . 2 (𝜑𝜓)
31, 2sylg 1748 1 (𝜑 → ∀𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1479 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1720  ax-4 1735 This theorem is referenced by:  nexdh  1790  albidh  1791  alrimiv  1853  ax12i  1877  cbvaliw  1931  nf5dh  2024  alrimi  2080  hbnd  2145  alrimiOLD  2190  cbvalv  2271  aevALTOLD  2319  eujustALT  2471  axi5r  2592  hbralrimi  2951  bnj1093  31022  bj-abv  32876  bj-ab0  32877  mpt2bi123f  33942  axc4i-o  34002  equidq  34028  aev-o  34035  ax12f  34044  axc5c4c711  38422  hbimpg  38590  gen11nv  38662
 Copyright terms: Public domain W3C validator