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

Theorem r19.26 2486
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 2427 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 108 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2427 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 300 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 137 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2428 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 122 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 124 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103  wral 2349
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 1377  ax-gen 1379
This theorem depends on definitions:  df-bi 115  df-ral 2354
This theorem is referenced by:  r19.26-2  2487  r19.26-3  2488  ralbiim  2492  r19.27av  2493  reu8  2789  ssrab  3073  r19.28m  3332  r19.27m  3338  2ralunsn  3592  iuneq2  3696  cnvpom  4884  funco  4964  fncnv  4990  funimaexglem  5007  fnres  5040  fnopabg  5047  mpteqb  5287  eqfnfv3  5293  caoftrn  5761  iinerm  6237  rexanuz  10001  recvguniq  10008  cau3lem  10127  rexanre  10233  bezoutlemmo  10528  sqrt2irr  10674  bj-indind  10870
  Copyright terms: Public domain W3C validator