New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  19.26 GIF version

Theorem 19.26 1593
 Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
19.26 (x(φ ψ) ↔ (xφ xψ))

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 443 . . . 4 ((φ ψ) → φ)
21alimi 1559 . . 3 (x(φ ψ) → xφ)
3 simpr 447 . . . 4 ((φ ψ) → ψ)
43alimi 1559 . . 3 (x(φ ψ) → xψ)
52, 4jca 518 . 2 (x(φ ψ) → (xφ xψ))
6 id 19 . . 3 ((φ ψ) → (φ ψ))
76alanimi 1562 . 2 ((xφ xψ) → x(φ ψ))
85, 7impbii 180 1 (x(φ ψ) ↔ (xφ xψ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  19.26-2  1594  19.26-3an  1595  19.35  1600  19.43OLD  1606  albiim  1611  2albiim  1612  19.27  1869  19.28  1870  ax12olem2  1928  ax11eq  2193  ax11el  2194  2eu4  2287  bm1.1  2338  r19.26m  2749  unss  3437  ralunb  3444  ssin  3477  intun  3958  intpr  3959  eqopr  4847
 Copyright terms: Public domain W3C validator