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

Theorem alrimih 1791
 Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2113 and 19.21h 2159. Instance of sylg 1790. (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 1790 1 (𝜑 → ∀𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1762  ax-4 1777 This theorem is referenced by:  nexdh  1832  albidh  1833  alrimiv  1895  ax12i  1936  cbvaliw  1979  nf5dh  2066  alrimi  2120  hbnd  2185  alrimiOLD  2228  cbvalv  2309  eujustALT  2501  axi5r  2623  hbralrimi  2983  bnj1093  31174  bj-abv  33026  bj-ab0  33027  mpt2bi123f  34101  axc4i-o  34502  equidq  34528  aev-o  34535  ax12f  34544  axc5c4c711  38919  hbimpg  39087  gen11nv  39159
 Copyright terms: Public domain W3C validator