Theorem impexp 276

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.

Assertion

Ref	Expression
impexp	|- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		df-an 198	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	imbi1i 161	. 2 |- (((ph /\ ps) -> ch) <-> (-. (ph -> -. ps) -> ch))
3		expt 123	. . 3 |- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
4		impt 122	. . 3 |- ((ph -> (ps -> ch)) -> (-. (ph -> -. ps) -> ch))
5	3, 4	impbi 139	. 2 |- ((-. (ph -> -. ps) -> ch) <-> (ph -> (ps -> ch)))
6	2, 5	bitr 151	1 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  imp3a 279  imp4a 282  exp3a 292  exp4a 295  anass 336  orcana 509  nan 514  mo 1020  eu2 1023  moanim 1051  r2al 1231  r3al 1240  r19.23v 1282  reu2 1338  zfrep3 1476  inssdif0 1754  unissb 1941  elintrab 1977  dfiin2 2015  iunss 2017  dftr5 2044  dfom2 2374  fununi 2705  f1fv 2916  aceq1 3552  kmlem4 3583  iscard2 3660  suppsr3 4018  nnwos 4610  zmin 4617  chsscm 5147  chcmh 5148  h1det 5455  mdbr3 5729  mdbr4 5730  elat2 5739

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org