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

Theorem 19.21bi 1466
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 1416 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1416
This theorem is referenced by:  19.21bbi  1467  ax11e  1693  eqeq1  2062  eleq2  2117  r19.21bi  2424  elrab3t  2719  ssel  2966  copsex2t  4009  pocl  4067  ordsucim  4253  peano2  4345  funmo  4944  funun  4971  fununi  4994  imain  5008  tfrlem3-2d  5958  findcard  6375  findcard2  6376  findcard2s  6377
  Copyright terms: Public domain W3C validator