MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a4i Unicode version

Theorem a4i 1699
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
a4i.1  |-  A. x ph
Assertion
Ref Expression
a4i  |-  ph

Proof of Theorem a4i
StepHypRef Expression
1 a4i.1 . 2  |-  A. x ph
2 ax-4 1692 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 10 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1532
This theorem is referenced by:  equid  1818  darii  2215  barbari  2217  cesare  2219  camestres  2220  festino  2221  baroco  2222  cesaro  2223  camestros  2224  datisi  2225  disamis  2226  felapton  2229  darapti  2230  calemes  2231  dimatis  2232  fresison  2233  calemos  2234  fesapo  2235  bamalip  2236  kmlem2  7710  axac2  8026  axac  8027  axaci  8028  ballotlem2  22973  axlmp2  24356  axlmp3  24357  bnj864  27966
This theorem was proved from axioms:  ax-mp 10  ax-4 1692
  Copyright terms: Public domain W3C validator