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 2127  inssdif0 2337  unissb 2532  elintrab 2549  dfiin2 2592  iunss 2595  dftr5 2688  axrep5 2703  ordunisuc2 3121  dfom2 3139  asymref2 3446  fununi 3569  f1fv 3880  oaabs 4258  aceq1 4739  iscard2 4865  suppsr3 5236  infm3 6056  infmsup 6070  primet 6197  zmin 6221  ralrp 6290  raluz 6443  raluz2 6444  nnwos 6461  cau4i 6918  cau5 6919  cvg2 6922  cvg3 6923  facwordit 6944  clm4 7080  caucvg 7163  tgss3t 7637  islp2 7744  cncnplem3 7773  cncfmet 7902  metcnp4 7967  metcn4 7968  nmobndseqi 8436  grothprim 8778  chsscm 9107  chcmh 9108  h1det 9468  mdsl1 10243  mdsl2 10244  elat2 10262

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