Theorem impexp 345

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 223	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	imbi1i 184	. 2 |- (((ph /\ ps) -> ch) <-> (-. (ph -> -. ps) -> ch))
3		expt 140	. . 3 |- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
4		impt 139	. . 3 |- ((ph -> (ps -> ch)) -> (-. (ph -> -. ps) -> ch))
5	3, 4	impbii 155	. 2 |- ((-. (ph -> -. ps) -> ch) <-> (ph -> (ps -> ch)))
6	2, 5	bitri 171	1 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  pm3.3 346  pm3.31 347  imp 348  pm4.14 350  pm4.15 351  pm4.78 352  pm4.87 354  imp3a 359  imp4a 362  ex 371  exp3a 374  exp4a 378  anass 441  pm5.6 692  nan 693  2sb6 1375  2sb6rf 1378  2exsb 1390  mo 1432  eu2 1435  moanim 1466  2mo 1487  2eu6 1494  r2al 1722  r3al 1736  r19.23v 1787  reu2 1976  reu6 1978  rmo4 1979  rabss 2176  inssdif0 2386  unissb 2595  elintrab 2612  dfiin2 2656  iunss 2659  dftr5 2757  axrep5 2772  ordunisuc2 3198  dfom2 3220  asymref2 3532  fununi 3668  dff13 3988  oaabs 4392  aceq1 4875  iscard2 5004  suppsr3 5378  ralrp 6205  infm3 6222  infmsup 6236  prime 6366  zmin 6391  raluz 6569  raluz2 6570  nnwos 6587  cau4ii 7121  cau5i 7122  cvg2i 7125  cvg3i 7126  facwordi 7147  clm4i 7283  caucvgi 7366  tgss3 7850  islp2 7957  cncnplem3 7986  cncfmet 8116  metcnp4 8181  metcn4 8182  nmobndseqi 8695  grothprim 9057  chsscmi 9388  chcmhi 9389  h1dei 9749  mdsl1i 10529  mdsl2i 10530  elat2 10548  elicc3 11410  cnfillim 11687  flimfcn 11715  fcluscn 11731  fclsfcn 11744  lmclim2 11915  lmtlm 11969  heiborlem16 12026

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

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain