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  2212  barbari  2214  cesare  2216  camestres  2217  festino  2218  baroco  2219  cesaro  2220  camestros  2221  datisi  2222  disamis  2223  felapton  2226  darapti  2227  calemes  2228  dimatis  2229  fresison  2230  calemos  2231  fesapo  2232  bamalip  2233  kmlem2  7661  axac2  7977  axac  7978  axaci  7979  axlmp2  24190  axlmp3  24191  bnj864  27643
This theorem was proved from axioms:  ax-mp 10  ax-4 1692
  Copyright terms: Public domain W3C validator