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

Theorem reximdv 2414
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
Hypothesis
Ref Expression
reximdv.1 (φ → (ψχ))
Assertion
Ref Expression
reximdv (φ → (x A ψx A χ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)   A(x)

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3 (φ → (ψχ))
21a1d 22 . 2 (φ → (x A → (ψχ)))
32reximdvai 2413 1 (φ → (x A ψx A χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  wrex 2301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306
This theorem is referenced by:  r19.12  2416  reusv3  4158  rexxfrd  4161  iunpw  4177  fvelima  5168  prnmaddl  6472  prarloclem5  6482  prarloc2  6486  genprndl  6504  genprndu  6505  ltpopr  6567  recexprlemm  6594  recexprlemopl  6595  recexprlemopu  6597  recexprlem1ssl  6603  recexprlem1ssu  6604
  Copyright terms: Public domain W3C validator