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 687  nan 688  2sb6 1334  2sb6rf 1337  2exsb 1349  mo 1391  eu2 1394  moanim 1425  2mo 1445  2eu6 1452  r2al 1673  r3al 1687  r19.23v 1738  reu2 1926  reu6 1928  rmo4 1929  rabss 2120  inssdif0 2329  unissb 2523  elintrab 2540  dfiin2 2583  iunss 2586  dftr5 2678  axrep5 2693  ordunisuc2 3110  dfom2 3128  asymref2 3432  fununi 3555  f1fv 3865  oaabs 4242  aceq1 4709  iscard2 4834  suppsr3 5204  infm3 6009  infmsup 6023  primet 6150  zmin 6175  ralrp 6234  raluz 6382  raluz2 6383  nnwos 6400  cau4i 6863  cau5 6864  cvg2 6867  cvg3 6868  facwordit 6889  clm4 7026  caucvg 7107  tgss3t 7588  islp2 7697  cncnplem3 7726  cncfmet 7857  metcnp4 7920  metcn4 7921  nmobndseqi 8385  grothprim 8722  chsscm 9051  chcmh 9052  h1det 9411  mdsl1 10185  mdsl2 10186  elat2 10204

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