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

Theorem 19.26 1458
 Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
19.26 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 108 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1432 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 109 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1432 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 304 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1436 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 125 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∀wal 1330 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 1424  ax-gen 1426 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  19.26-2  1459  19.26-3an  1460  albiim  1464  2albiim  1465  hband  1466  hban  1527  19.27h  1540  19.27  1541  19.28h  1542  19.28  1543  nford  1547  nfand  1548  equsexd  1708  equveli  1733  sbanv  1862  2eu4  2093  bm1.1  2125  r19.26m  2566  unss  3254  ralunb  3261  ssin  3302  intun  3809  intpr  3810  eqrelrel  4647  relop  4696  eqoprab2b  5836  dfer2  6437  omniwomnimkv  7048
 Copyright terms: Public domain W3C validator