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

Theorem r19.26 2497
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 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 107 . . . 4 ((𝜑𝜓) → 𝜑)
21ralimi 2438 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 108 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2438 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 300 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 137 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2439 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 122 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 124 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  r19.26-2  2498  r19.26-3  2499  ralbiim  2503  r19.27av  2504  reu8  2809  ssrab  3097  r19.28m  3367  r19.27m  3373  2ralunsn  3637  iuneq2  3741  cnvpom  4960  funco  5040  fncnv  5066  funimaexglem  5083  fnres  5116  fnopabg  5123  mpteqb  5377  eqfnfv3  5383  caoftrn  5862  iinerm  6344  rexanuz  10386  recvguniq  10393  cau3lem  10512  rexanre  10618  bezoutlemmo  11077  sqrt2irr  11223  bj-indind  11473
  Copyright terms: Public domain W3C validator