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

Theorem alrimih 1827
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21h 2284. Instance of sylg 1826. (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 1826 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812
This theorem is referenced by:  nexdh  1869  albidh  1870  alrimiv  1931  ax12i  1971  cbvaliw  2010  nf5dh  2144  alrimi  2207  hbnd  2293  cbv3v  2332  cbv3  2396  eujustALT  2567  axi5r  2696  hbralrimi  3138  ralidmw  4466  bnj1093  33649  bj-abvALT  35420  bj-gabssd  35452  mpobi123f  36667  axc4i-o  37406  equidq  37432  aev-o  37439  ax12f  37448  axc5c4c711  42769  hbimpg  42924  gen11nv  42987
  Copyright terms: Public domain W3C validator