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 376  exp4a 380  anass 441  pm5.6 690  nan 691  2sb6 1338  2sb6rf 1341  2exsb 1353  mo 1395  eu2 1398  moanim 1429  2mo 1450  2eu6 1457  r2al 1679  r3al 1693  r19.23v 1744  reu2 1933  reu6 1935  rmo4 1936  rabss 2128  inssdif0 2338  unissb 2533  elintrab 2550  dfiin2 2593  iunss 2596  dftr5 2689  axrep5 2704  ordunisuc2 3122  dfom2 3140  asymref2 3447  fununi 3570  f1fv 3881  oaabs 4259  aceq1 4746  iscard2 4872  suppsr3 5243  infm3 6063  infmsup 6077  primet 6204  zmin 6228  ralrp 6297  raluz 6450  raluz2 6451  nnwos 6468  cau4i 6925  cau5 6926  cvg2 6929  cvg3 6930  facwordit 6951  clm4 7087  caucvg 7170  tgss3t 7644  islp2 7751  cncnplem3 7780  cncfmet 7909  metcnp4 7974  metcn4 7975  nmobndseqi 8443  grothprim 8785  chsscm 9114  chcmh 9115  h1det 9475  mdsl1 10251  mdsl2 10252  elat2 10270

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