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

Theorem alrimih 1824
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2207 and 19.21h 2295. Instance of sylg 1823. (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 1823 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535
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  1969  cbvaliw  2013  nf5dh  2151  alrimi  2213  sbbibOLD  2289  hbnd  2304  cbv3v  2355  cbv3  2415  cbvalvOLD  2420  eujustALT  2656  axi5r  2784  hbralrimi  3167  bnj1093  32260  bj-abv  34240  bj-ab0  34241  mpobi123f  35476  axc4i-o  36070  equidq  36096  aev-o  36103  ax12f  36112  axc5c4c711  40888  hbimpg  41043  gen11nv  41106
  Copyright terms: Public domain W3C validator