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

Theorem 19.26 1415
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 1389 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 108 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1389 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 300 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1393 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 124 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103  wal 1287
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 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.26-2  1416  19.26-3an  1417  albiim  1421  2albiim  1422  hband  1423  hban  1484  19.27h  1497  19.27  1498  19.28h  1499  19.28  1500  nford  1504  nfand  1505  equsexd  1664  equveli  1689  sbanv  1817  2eu4  2041  bm1.1  2073  r19.26m  2500  unss  3172  ralunb  3179  ssin  3220  intun  3714  intpr  3715  eqrelrel  4527  relop  4574  eqoprab2b  5689  dfer2  6273
  Copyright terms: Public domain W3C validator