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  26944  3ax5  27090  3ax5VD  27425  hbalgVD  27468  alimiK  27895  alimdK  27897  alimdvK  27898  a4imK  27903  a4imvK  27904  ax4wfK  27905  ax4wK  27906  a16gALTX  28002
  Copyright terms: Public domain W3C validator