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

Theorem 19.21bi 1432
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 1381 . 2 (xψψ)
31, 2syl 14 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1381
This theorem is referenced by:  19.21bbi  1433  ax11e  1659  eqeq1  2028  eleq2  2083  r19.21bi  2385  elrab3t  2674  ssel  2916  copsex2t  3956  pocl  4014  ordsucim  4176  peano2  4245  funmo  4843  funun  4870  fununi  4893  imain  4907  tfrlem3-2d  5850
  Copyright terms: Public domain W3C validator