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

Theorem 19.21bi 1522
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 1472 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1472
This theorem is referenced by:  19.21bbi  1523  ax11e  1752  eqeq1  2124  eleq2  2181  r19.21bi  2497  elrab3t  2812  ssel  3061  exmidsssn  4095  copsex2t  4137  pocl  4195  ordsucim  4386  peano2  4479  funmo  5108  funun  5137  fununi  5161  imain  5175  tfrlem3-2d  6177  tfr1onlemaccex  6213  tfri1dALT  6216  tfrcllemaccex  6226  findcard  6750  findcard2  6751  findcard2s  6752  exmidpw  6770
  Copyright terms: Public domain W3C validator