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

Theorem 19.21bi 1537
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 1487 . 2 (∀𝑥𝜓𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1487
This theorem is referenced by:  19.21bbi  1538  ax11e  1768  eqeq1  2144  eleq2  2201  r19.21bi  2518  elrab3t  2834  ssel  3086  exmidsssn  4120  copsex2t  4162  pocl  4220  ordsucim  4411  peano2  4504  funmo  5133  funun  5162  fununi  5186  imain  5200  tfrlem3-2d  6202  tfr1onlemaccex  6238  tfri1dALT  6241  tfrcllemaccex  6251  findcard  6775  findcard2  6776  findcard2s  6777  exmidpw  6795
  Copyright terms: Public domain W3C validator