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

Theorem 19.21bi 1447
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
19.21bi.1 (φxψ)
Assertion
Ref Expression
19.21bi (φψ)

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2 (φxψ)
2 ax-4 1397 . 2 (xψψ)
31, 2syl 14 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1397
This theorem is referenced by:  19.21bbi  1448  ax11e  1674  eqeq1  2043  eleq2  2098  r19.21bi  2401  elrab3t  2691  ssel  2933  copsex2t  3973  pocl  4031  ordsucim  4192  peano2  4261  funmo  4860  funun  4887  fununi  4910  imain  4924  tfrlem3-2d  5869
  Copyright terms: Public domain W3C validator