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

Theorem r19.26 2438
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 2381 . . 3 (x A (φ ψ) → x A φ)
3 simpr 103 . . . 4 ((φ ψ) → ψ)
43ralimi 2381 . . 3 (x A (φ ψ) → x A ψ)
52, 4jca 290 . 2 (x A (φ ψ) → (x A φ x A ψ))
6 pm3.2 126 . . . 4 (φ → (ψ → (φ ψ)))
76ral2imi 2382 . . 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 2303
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 1336  ax-gen 1338
This theorem depends on definitions:  df-bi 110  df-ral 2308
This theorem is referenced by:  r19.26-2  2439  r19.26-3  2440  ralbiim  2444  r19.27av  2445  reu8  2734  ssrab  3015  r19.28m  3308  r19.27m  3313  2ralunsn  3563  iuneq2  3667  cnvpom  4806  funco  4886  fncnv  4911  funimaexglem  4928  fnres  4961  fnopabg  4968  mpteqb  5207  eqfnfv3  5213  caoftrn  5681  iinerm  6118  bj-indind  9499
  Copyright terms: Public domain W3C validator