Theorem impexp 374

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 242	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	imbi1i 203	. 2 |- (((ph /\ ps) -> ch) <-> (-. (ph -> -. ps) -> ch))
3		expt 159	. . 3 |- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
4		impt 158	. . 3 |- ((ph -> (ps -> ch)) -> (-. (ph -> -. ps) -> ch))
5	3, 4	impbii 174	. 2 |- ((-. (ph -> -. ps) -> ch) <-> (ph -> (ps -> ch)))
6	2, 5	bitri 190	1 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm3.3 375  pm3.31 376  imp 377  pm4.14 379  pm4.15 380  pm4.78 381  pm4.87 383  imp3a 388  imp4a 391  ex 402  exp3a 405  exp4a 409  anass 487  pm5.3 494  pm5.6 752  nan 753  impexp3a 1292  2sb6 1726  2sb6rf 1729  2exsb 1742  mo 1787  eu2 1791  moanim 1826  2mo 1851  2eu6 1858  r2al 2136  r3al 2151  r19.23 2206  r19.23OLD 2207  ralrab 2418  euind 2439  reu2 2442  reu3 2444  rmo4 2445  reuind 2450  rabss 2684  inssdif0OLD 2941  unissb 3208  elintrab 3228  dfiin2OLD 3288  iunssOLD 3292  dftr5 3414  axrep5 3433  eufromeq4 3831  ordunisuc2 3926  dfom2 3951  asymref2OLD 4311  fununi 4481  dff13 4850  oaabs 5309  aceq1 5891  iscard2 6006  suppsr3 6376  ralrp 7246  infm3 7263  infmsup 7277  prime 7407  zmin 7432  raluz 7611  raluz2 7612  nnwos 7629  cau4ii 8170  cau5i 8171  cvg2i 8174  cvg3i 8175  facwordi 8196  clm4i 8340  caucvgi 8423  tgss3 8908  islp2 9023  cncnplem3 9053  cncfmet 9183  metcnp4 9248  metcn4 9249  nmobndseqi 9780  axgroth6 10137  grothprim 10141  chsscmi 10745  chcmhi 10746  h1dei 11106  mdsl1i 11893  mdsl2i 11894  elat2 11912  bnj112 12457  bnj115 12459  bnj856 12789  bnj861 12794  bnj947 12846  bnj980 12862  bnj979 12863  bnj1048 12888  bnj1050 12889  bnj1054 12891  bnj1057 12894  bnj1087 12909  bnj1088 12910  bnj1091 12912  bnj1092 12913  bnj580 13301  bnj1049 13394  bnj1070 13401  bnj1171 13439  imim21b 13597  isprm2 13775  axextprim 13785  biimpexp 13815  dffr5 13831  dfon2lem8 13856  predreseq 13890  elicc3 15362  cnfillim 15590  flimfcn 15603  fcluscn 15619  fclsfcn 15632  ralrabOLD 15670  lmclim2 15850  lmtlm 15908  heiborlem16 15970  pm11.62 16351  dfvd2 16490  dfvd3 16495

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 164  df-an 242

Copyright terms: Public domain