Theorem impexp 450

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Assertion

Ref	Expression
impexp	⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 448	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 449	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 209	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  imdistan  567  pm4.14  806  nan  829  pm4.87  843  pm5.6  1003  2sb6  2091  r2allem  3124  r3al  3174  r19.23t  3232  ceqsralt  3475  rspc2gv  3586  ralrab  3652  ralrab2  3656  euind  3682  reu2  3683  reu3  3685  rmo4  3688  rmo3f  3692  reuind  3711  2reu5lem3  3715  rmo2  3837  rmo3  3839  rmoanim  3844  rmoanimALT  3845  ralss  4008  ralssOLD  4010  rabss  4022  raldifb  4101  ralin  4201  rabsssn  4625  raldifsni  4751  unissb  4896  elintrab  4915  ssintrab  4926  dftr5  5209  axrep5  5232  reusv2lem4  5346  reusv2  5348  reusv3  5350  raliunxp  5788  dfpo2  6254  fununi  6567  fvn0ssdmfun  7019  dff13  7200  ordunisuc2  7786  dfom2  7810  frpoins3xpg  8082  frpoins3xp3g  8083  xpord2indlem  8089  xpord3inddlem  8096  dfsmo2  8279  qliftfun  8739  dfsup2  9347  wemapsolem  9455  iscard2  9888  acnnum  9962  aceq1  10027  dfac9  10047  dfacacn  10052  axgroth6  10739  sstskm  10753  infm3  12101  prime  12573  raluz  12809  raluz2  12810  nnwos  12828  ralrp  12927  facwordi  14212  cotr2g  14899  rexuzre  15276  limsupgle  15400  ello12  15439  elo12  15450  lo1resb  15487  rlimresb  15488  o1resb  15489  modfsummod  15717  isprm2  16609  isprm4  16611  isprm7  16635  acsfn2  17586  pgpfac1  20011  isirred2  20357  isdomn2OLD  20645  isdomn3  20648  islindf4  21793  coe1fzgsumd  22248  evl1gsumd  22301  ist1-2  23291  isnrm2  23302  dfconn2  23363  1stccn  23407  iskgen3  23493  hausdiag  23589  cnflf  23946  txflf  23950  cnfcf  23986  metcnp  24485  caucfil  25239  ovolgelb  25437  ismbl  25483  dyadmbllem  25556  itg2leub  25691  ellimc3  25836  mdegleb  26025  jensen  26955  dchrelbas2  27204  dchrelbas3  27205  eqcuts2  27782  onsis  28270  ons2ind  28271  nmoubi  30847  nmobndseqi  30854  nmobndseqiALT  30855  h1dei  31625  nmopub  31983  nmfnleub  32000  mdsl1i  32396  mdsl2i  32397  elat2  32415  rabsspr  32576  rabsstp  32577  islinds5  33448  islbs5  33461  eulerpartlemgvv  34533  bnj115  34881  bnj1109  34942  bnj1533  35008  bnj580  35069  bnj864  35078  bnj865  35079  bnj1049  35130  bnj1090  35135  bnj1093  35136  bnj1133  35145  bnj1171  35156  climuzcnv  35865  axextprim  35895  biimpexp  35911  dfon2lem8  35982  dffun10  36106  filnetlem4  36575  bj-substax12  36922  wl-2sb6d  37759  poimirlem25  37842  poimirlem30  37847  r2alan  38443  inxpss  38506  moantr  38553  isat3  39563  isltrn2N  40376  cdlemefrs29bpre0  40652  cdleme32fva  40693  sn-axrep5v  42469  dford4  43267  fnwe2lem2  43289  ifpidg  43728  ifpim23g  43732  elmapintrab  43813  undmrnresiss  43841  df3or2  44005  df3an2  44006  dfhe3  44012  dffrege76  44176  dffrege115  44215  ntrneiiso  44328  ismnushort  44538  pm11.62  44631  2sbc6g  44652  expcomdg  44737  impexpd  44750  dfvd2  44816  dfvd3  44828  modelac8prim  45229  rabssf  45359  2rexsb  47343  2rexrsb  47344  snlindsntor  48713  elbigo2  48794  exp12bd  49037  ralbidb  49041  ralbidc  49042