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

Theorem r19.26 2517
 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 2454 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 109 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2454 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 302 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 138 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2456 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 123 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 125 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∀wral 2375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393 This theorem depends on definitions:  df-bi 116  df-ral 2380 This theorem is referenced by:  r19.27v  2518  r19.28v  2519  r19.26-2  2520  r19.26-3  2521  ralbiim  2525  r19.27av  2526  reu8  2833  ssrab  3122  r19.28m  3399  r19.27m  3405  2ralunsn  3672  iuneq2  3776  cnvpom  5017  funco  5099  fncnv  5125  funimaexglem  5142  fnres  5175  fnopabg  5182  mpteqb  5443  eqfnfv3  5452  caoftrn  5938  iinerm  6431  ixpeq2  6536  ixpin  6547  rexanuz  10600  recvguniq  10607  cau3lem  10726  rexanre  10832  bezoutlemmo  11487  sqrt2irr  11633  tgval2  12002  metequiv  12423  metequiv2  12424  mulcncflem  12502  bj-indind  12715
 Copyright terms: Public domain W3C validator