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

Axiom ax-5 1533
Description: Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-5  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )

Detailed syntax breakdown of Axiom ax-5
StepHypRef Expression
1 wph . . . 4  wff  ph
2 wps . . . 4  wff  ps
31, 2wi 6 . . 3  wff  ( ph  ->  ps )
4 vx . . 3  set  x
53, 4wal 1532 . 2  wff  A. x
( ph  ->  ps )
61, 4wal 1532 . . 3  wff  A. x ph
72, 4wal 1532 . . 3  wff  A. x ps
86, 7wi 6 . 2  wff  ( A. x ph  ->  A. x ps )
95, 8wi 6 1  wff  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
Colors of variables: wff set class
This axiom is referenced by:  alimi  1546  alim  1548  a16gALT  1679  ax4  1691  ax5o  1693  stoweidlem61  27131  3ax5  27337  3ax5VD  27672  hbalgVD  27715  alimiK  28142  alimdK  28144  alimdvK  28145  a4imK  28150  a4imvK  28151  ax4wfK  28152  ax4wK  28153  a16gALTX  28249
  Copyright terms: Public domain W3C validator