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

Theorem alrimih 1741
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2062 and 19.21h 2107. Instance of sylg 1740. (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 1740 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728
This theorem is referenced by:  nexdh  1779  albidh  1780  exbidhOLD  1782  alrimiv  1842  ax12i  1866  cbvaliw  1920  nf5dh  2013  alrimi  2069  hbnd  2132  cbv3hvOLD  2161  alrimiOLD  2180  aevALTOLD  2309  eujustALT  2461  axi5r  2582  hbralrimi  2937  bnj1093  30302  bj-ax12iOLD  31804  bj-abv  32093  bj-ab0  32094  mpt2bi123f  33141  axc4i-o  33201  equidq  33227  aev-o  33234  ax12f  33243  axc5c4c711  37624  hbimpg  37791  gen11nv  37863
  Copyright terms: Public domain W3C validator