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

Theorem 19.26 1438
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 1412 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 109 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1412 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 302 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1416 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 125 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wal 1310
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 1404  ax-gen 1406
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.26-2  1439  19.26-3an  1440  albiim  1444  2albiim  1445  hband  1446  hban  1507  19.27h  1520  19.27  1521  19.28h  1522  19.28  1523  nford  1527  nfand  1528  equsexd  1688  equveli  1713  sbanv  1841  2eu4  2066  bm1.1  2098  r19.26m  2535  unss  3214  ralunb  3221  ssin  3262  intun  3766  intpr  3767  eqrelrel  4598  relop  4647  eqoprab2b  5781  dfer2  6382
  Copyright terms: Public domain W3C validator