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

Theorem ralimia 3080
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
ralimia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralimia (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimia
StepHypRef Expression
1 ralimia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21a2i 14 . 2 ((𝑥𝐴𝜑) → (𝑥𝐴𝜓))
32ralimi2 3079 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2131  wral 3042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878
This theorem depends on definitions:  df-bi 197  df-ral 3047
This theorem is referenced by:  ralimiaa  3081  ralimi  3082  r19.12  3193  rr19.3v  3477  rr19.28v  3478  exfo  6532  ffvresb  6549  f1mpt  6673  weniso  6759  ixpf  8088  ixpiunwdom  8653  tz9.12lem3  8817  dfac2a  9134  kmlem12  9167  axdc2lem  9454  ac6num  9485  ac6c4  9487  brdom6disj  9538  konigthlem  9574  arch  11473  cshw1  13760  serf0  14602  symgextfo  18034  baspartn  20952  ptcnplem  21618  spanuni  28704  lnopunilem1  29170  phpreu  33698  finixpnum  33699  poimirlem26  33740  indexa  33833  heiborlem5  33919  rngmgmbs4  34035  mzpincl  37791  dfac11  38126  stgoldbwt  42166  2zrngnmlid2  42453
  Copyright terms: Public domain W3C validator