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

Theorem r19.26 2410
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26 (x A (φ ψ) ↔ (x A φ x A ψ))

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 102 . . . 4 ((φ ψ) → φ)
21ralimi 2353 . . 3 (x A (φ ψ) → x A φ)
3 simpr 103 . . . 4 ((φ ψ) → ψ)
43ralimi 2353 . . 3 (x A (φ ψ) → x A ψ)
52, 4jca 290 . 2 (x A (φ ψ) → (x A φ x A ψ))
6 pm3.2 126 . . . 4 (φ → (ψ → (φ ψ)))
76ral2imi 2354 . . 3 (x A φ → (x A ψx A (φ ψ)))
87imp 115 . 2 ((x A φ x A ψ) → x A (φ ψ))
95, 8impbii 117 1 (x A (φ ψ) ↔ (x A φ x A ψ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98  wral 2275
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 1309  ax-gen 1311
This theorem depends on definitions:  df-bi 110  df-ral 2280
This theorem is referenced by:  r19.26-2  2411  r19.26-3  2412  ralbiim  2416  r19.27av  2417  reu8  2705  ssrab  2986  r19.28m  3279  r19.27m  3284  2ralunsn  3532  iuneq2  3636  cnvpom  4775  funco  4854  fncnv  4879  funimaexglem  4896  fnres  4929  fnopabg  4936  mpteqb  5174  eqfnfv3  5180  caoftrn  5647  iinerm  6077
  Copyright terms: Public domain W3C validator