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

Theorem alrimih 1830
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2209 and 19.21h 2291. Instance of sylg 1829. (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 1829 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 1802  ax-4 1816
This theorem is referenced by:  nexdh  1872  albidh  1873  alrimiv  1934  ax12i  1974  cbvaliw  2018  nf5dh  2151  alrimi  2215  hbnd  2300  cbv3v  2337  cbv3  2397  eujustALT  2573  axi5r  2702  hbralrimi  3094  ralidmw  4394  bnj1093  32531  bj-abvALT  34736  bj-gabssd  34767  mpobi123f  35963  axc4i-o  36555  equidq  36581  aev-o  36588  ax12f  36597  axc5c4c711  41577  hbimpg  41732  gen11nv  41795
  Copyright terms: Public domain W3C validator