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

Theorem r19.26 2456
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 106 . . . 4 ((𝜑𝜓) → 𝜑)
21ralimi 2399 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 107 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2399 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 294 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 130 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2400 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 119 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 121 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102  wral 2321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352
This theorem depends on definitions:  df-bi 114  df-ral 2326
This theorem is referenced by:  r19.26-2  2457  r19.26-3  2458  ralbiim  2462  r19.27av  2463  reu8  2757  ssrab  3043  r19.28m  3336  r19.27m  3341  2ralunsn  3594  iuneq2  3698  cnvpom  4885  funco  4965  fncnv  4990  funimaexglem  5007  fnres  5040  fnopabg  5047  mpteqb  5286  eqfnfv3  5292  caoftrn  5761  iinerm  6206  rexanuz  9779  recvguniq  9785  cau3lem  9904  sqrt2irr  10194  bj-indind  10386
  Copyright terms: Public domain W3C validator