New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  r19.26 GIF version

Theorem r19.26 2746
 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 443 . . . 4 ((φ ψ) → φ)
21ralimi 2689 . . 3 (x A (φ ψ) → x A φ)
3 simpr 447 . . . 4 ((φ ψ) → ψ)
43ralimi 2689 . . 3 (x A (φ ψ) → x A ψ)
52, 4jca 518 . 2 (x A (φ ψ) → (x A φ x A ψ))
6 pm3.2 434 . . . 4 (φ → (ψ → (φ ψ)))
76ral2imi 2690 . . 3 (x A φ → (x A ψx A (φ ψ)))
87imp 418 . 2 ((x A φ x A ψ) → x A (φ ψ))
95, 8impbii 180 1 (x A (φ ψ) ↔ (x A φ x A ψ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∀wral 2614 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2619 This theorem is referenced by:  r19.26-2  2747  r19.26-3  2748  ralbiim  2751  r19.27av  2752  r19.35  2758  reu8  3032  ssrab  3344  r19.28z  3642  r19.28zv  3645  r19.27z  3648  r19.27zv  3649  2ralunsn  3880  iuneq2  3985  fncnv  5158  fnres  5199  fnopabg  5205  eqfnfv3  5394
 Copyright terms: Public domain W3C validator