ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.21bi GIF version

Theorem 19.21bi 1569
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
19.21bi.1 (𝜑 → ∀𝑥𝜓)
Assertion
Ref Expression
19.21bi (𝜑𝜓)

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2 (𝜑 → ∀𝑥𝜓)
2 ax-4 1521 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1521
This theorem is referenced by:  19.21bbi  1570  ax11e  1807  eqeq1  2196  eleq2  2253  r19.21bi  2578  elrab3t  2907  ssel  3164  exmidsssn  4220  copsex2t  4263  pocl  4321  ordsucim  4517  peano2  4612  funmo  5250  funun  5279  fununi  5303  imain  5317  tfrlem3-2d  6338  tfr1onlemaccex  6374  tfri1dALT  6377  tfrcllemaccex  6387  findcard  6917  findcard2  6918  findcard2s  6919  exmidpw  6937  exmidpweq  6938
  Copyright terms: Public domain W3C validator