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

Theorem 19.21bi 1558
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 1510 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1510
This theorem is referenced by:  19.21bbi  1559  ax11e  1796  eqeq1  2184  eleq2  2241  r19.21bi  2565  elrab3t  2893  ssel  3150  exmidsssn  4203  copsex2t  4246  pocl  4304  ordsucim  4500  peano2  4595  funmo  5232  funun  5261  fununi  5285  imain  5299  tfrlem3-2d  6313  tfr1onlemaccex  6349  tfri1dALT  6352  tfrcllemaccex  6362  findcard  6888  findcard2  6889  findcard2s  6890  exmidpw  6908  exmidpweq  6909
  Copyright terms: Public domain W3C validator