Theorem impexp 347

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 225	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	imbi1i 186	. 2 |- (((ph /\ ps) -> ch) <-> (-. (ph -> -. ps) -> ch))
3		expt 142	. . 3 |- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
4		impt 141	. . 3 |- ((ph -> (ps -> ch)) -> (-. (ph -> -. ps) -> ch))
5	3, 4	impbi 157	. 2 |- ((-. (ph -> -. ps) -> ch) <-> (ph -> (ps -> ch)))
6	2, 5	bitr 173	1 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm3.3 348  pm3.31 349  imp 350  pm4.14 352  pm4.15 353  pm4.78 354  pm4.87 356  imp3a 361  imp4a 364  ex 373  exp3a 375  exp4a 378  anass 439  pm5.6 688  nan 689  2sb6 1336  2sb6rf 1339  2exsb 1351  mo 1393  eu2 1396  moanim 1427  2mo 1447  2eu6 1454  r2al 1676  r3al 1690  r19.23v 1741  reu2 1930  reu6 1932  rmo4 1933  rabss 2124  inssdif0 2333  unissb 2528  elintrab 2545  dfiin2 2588  iunss 2591  dftr5 2683  axrep5 2698  ordunisuc2 3115  dfom2 3133  asymref2 3440  fununi 3563  f1fv 3874  oaabs 4252  aceq1 4729  iscard2 4854  suppsr3 5224  infm3 6054  infmsup 6068  primet 6195  zmin 6219  ralrp 6289  raluz 6442  raluz2 6443  nnwos 6460  cau4i 6918  cau5 6919  cvg2 6922  cvg3 6923  facwordit 6944  clm4 7080  caucvg 7163  tgss3t 7638  islp2 7747  cncnplem3 7776  cncfmet 7905  metcnp4 7970  metcn4 7971  nmobndseqi 8440  grothprim 8783  chsscm 9112  chcmh 9113  h1det 9473  mdsl1 10248  mdsl2 10249  elat2 10267

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 147  df-an 225

Copyright terms: Public domain