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

Theorem alrimih 1739
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2059 and 19.21h 2104. Instance of sylg 1738. (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 1738 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1711  ax-4 1726
This theorem is referenced by:  nexdh  1777  albidh  1778  exbidhOLD  1780  alrimiv  1840  ax12i  1864  cbvaliw  1918  nf5dh  2011  alrimi  2066  hbnd  2129  cbv3hvOLD  2155  alrimiOLD  2174  aevALTOLD  2304  eujustALT  2456  axi5r  2577  hbralrimi  2932  bnj1093  30104  bj-ax12iOLD  31606  bj-abv  31892  bj-ab0  31893  mpt2bi123f  32940  axc4i-o  33000  equidq  33026  aev-o  33033  ax12f  33042  axc5c4c711  37423  hbimpg  37590  gen11nv  37662
  Copyright terms: Public domain W3C validator