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

Theorem 19.26 1411
 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 107 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1385 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 108 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1385 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 300 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1389 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 124 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 102   ↔ wb 103  ∀wal 1283 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 This theorem is referenced by:  19.26-2  1412  19.26-3an  1413  albiim  1417  2albiim  1418  hband  1419  hban  1480  19.27h  1493  19.27  1494  19.28h  1495  19.28  1496  nford  1500  nfand  1501  equsexd  1658  equveli  1683  sbanv  1811  2eu4  2035  bm1.1  2067  r19.26m  2489  unss  3147  ralunb  3154  ssin  3189  intun  3669  intpr  3670  eqrelrel  4461  relop  4508  eqoprab2b  5588  dfer2  6166
 Copyright terms: Public domain W3C validator