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

Theorem 19.21bi 1491
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 1441 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1441
This theorem is referenced by:  19.21bbi  1492  ax11e  1719  eqeq1  2089  eleq2  2146  r19.21bi  2454  elrab3t  2756  ssel  3002  copsex2t  4028  pocl  4086  ordsucim  4272  peano2  4364  funmo  4967  funun  4994  fununi  5018  imain  5032  tfrlem3-2d  5981  tfr1onlemaccex  6017  tfri1dALT  6020  tfrcllemaccex  6030  findcard  6444  findcard2  6445  findcard2s  6446
  Copyright terms: Public domain W3C validator