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

Theorem 19.26 1492
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 109 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1466 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 110 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1466 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 306 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1470 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 126 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  19.26-2  1493  19.26-3an  1494  albiim  1498  2albiim  1499  hband  1500  hban  1558  19.27h  1571  19.27  1572  19.28h  1573  19.28  1574  nford  1578  nfand  1579  equsexd  1740  equveli  1770  sbanv  1901  2eu4  2131  bm1.1  2174  r19.26m  2621  unss  3324  ralunb  3331  ssin  3372  intun  3890  intpr  3891  eqrelrel  4745  relop  4795  eqoprab2b  5955  dfer2  6561  omniwomnimkv  7196
  Copyright terms: Public domain W3C validator