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

Theorem r19.26 2558
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 108 . . . 4 ((𝜑𝜓) → 𝜑)
21ralimi 2495 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 109 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2495 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 304 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 138 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2497 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 123 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 125 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wral 2416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425
This theorem depends on definitions:  df-bi 116  df-ral 2421
This theorem is referenced by:  r19.27v  2559  r19.28v  2560  r19.26-2  2561  r19.26-3  2562  ralbiim  2566  r19.27av  2567  reu8  2880  ssrab  3175  r19.28m  3452  r19.27m  3458  2ralunsn  3725  iuneq2  3829  cnvpom  5081  funco  5163  fncnv  5189  funimaexglem  5206  fnres  5239  fnopabg  5246  mpteqb  5511  eqfnfv3  5520  caoftrn  6007  iinerm  6501  ixpeq2  6606  ixpin  6617  rexanuz  10774  recvguniq  10781  cau3lem  10900  rexanre  11006  bezoutlemmo  11707  sqrt2irr  11853  tgval2  12236  metequiv  12680  metequiv2  12681  mulcncflem  12775  bj-indind  13237
  Copyright terms: Public domain W3C validator