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

Theorem 19.26 1384
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 106 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1358 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 107 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1358 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 294 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1362 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 121 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102  wal 1255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  19.26-2  1385  19.26-3an  1386  albiim  1390  2albiim  1391  hband  1392  hban  1453  19.27h  1466  19.27  1467  19.28h  1468  19.28  1469  nford  1473  nfand  1474  equsexd  1631  equveli  1656  sbanv  1783  2eu4  2007  bm1.1  2039  r19.26m  2459  unss  3142  ralunb  3149  ssin  3184  intun  3671  intpr  3672  eqrelrel  4466  relop  4511  eqoprab2b  5588  dfer2  6135
  Copyright terms: Public domain W3C validator