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

Theorem 19.21bi 1495
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 1445 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1445
This theorem is referenced by:  19.21bbi  1496  ax11e  1724  eqeq1  2094  eleq2  2151  r19.21bi  2461  elrab3t  2770  ssel  3019  copsex2t  4072  pocl  4130  ordsucim  4317  peano2  4410  funmo  5030  funun  5058  fununi  5082  imain  5096  tfrlem3-2d  6077  tfr1onlemaccex  6113  tfri1dALT  6116  tfrcllemaccex  6126  findcard  6602  findcard2  6603  findcard2s  6604  exmidpw  6622
  Copyright terms: Public domain W3C validator