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

Theorem 19.26 1370
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 102 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1344 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 103 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1344 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 290 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1348 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 117 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 97  wb 98  wal 1241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  19.26-2  1371  19.26-3an  1372  albiim  1376  2albiim  1377  hband  1378  hban  1439  19.27h  1452  19.27  1453  19.28h  1454  19.28  1455  nford  1459  nfand  1460  equsexd  1617  equveli  1642  sbanv  1769  2eu4  1993  bm1.1  2025  r19.26m  2444  unss  3117  ralunb  3124  ssin  3159  intun  3646  intpr  3647  eqrelrel  4441  relop  4486  eqoprab2b  5563  dfer2  6107
  Copyright terms: Public domain W3C validator