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  2217  barbari  2219  cesare  2221  camestres  2222  festino  2223  baroco  2224  cesaro  2225  camestros  2226  datisi  2227  disamis  2228  felapton  2231  darapti  2232  calemes  2233  dimatis  2234  fresison  2235  calemos  2236  fesapo  2237  bamalip  2238  kmlem2  7745  axac2  8061  axac  8062  axaci  8063  ballotlem2  23009  axlmp2  24392  axlmp3  24393  bnj864  28086
This theorem was proved from axioms:  ax-mp 10  ax-4 1692
  Copyright terms: Public domain W3C validator