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  807  nan  830  pm4.87  844  pm5.6  1004  2sb6  2092  r2allem  3126  r3al  3176  r19.23t  3234  ceqsralt  3465  rspc2gv  3575  ralrab  3641  ralrab2  3645  euind  3671  reu2  3672  reu3  3674  rmo4  3677  rmo3f  3681  reuind  3700  2reu5lem3  3704  rmo2  3826  rmo3  3828  rmoanim  3833  rmoanimALT  3834  ralss  3997  ralssOLD  3999  rabss  4011  raldifb  4090  ralin  4190  rabsssn  4613  raldifsni  4739  unissb  4884  elintrab  4903  ssintrab  4914  dftr5  5197  axrep5  5220  reusv2lem4  5338  reusv2  5340  reusv3  5342  raliunxp  5788  dfpo2  6254  fununi  6567  fvn0ssdmfun  7020  dff13  7202  ordunisuc2  7788  dfom2  7812  frpoins3xpg  8083  frpoins3xp3g  8084  xpord2indlem  8090  xpord3inddlem  8097  dfsmo2  8280  qliftfun  8742  dfsup2  9350  wemapsolem  9458  iscard2  9891  acnnum  9965  aceq1  10030  dfac9  10050  dfacacn  10055  axgroth6  10742  sstskm  10756  infm3  12106  prime  12601  raluz  12837  raluz2  12838  nnwos  12856  ralrp  12955  facwordi  14242  cotr2g  14929  rexuzre  15306  limsupgle  15430  ello12  15469  elo12  15480  lo1resb  15517  rlimresb  15518  o1resb  15519  modfsummod  15748  isprm2  16642  isprm4  16644  isprm7  16669  acsfn2  17620  pgpfac1  20048  isirred2  20392  isdomn2OLD  20680  isdomn3  20683  islindf4  21828  coe1fzgsumd  22279  evl1gsumd  22332  ist1-2  23322  isnrm2  23333  dfconn2  23394  1stccn  23438  iskgen3  23524  hausdiag  23620  cnflf  23977  txflf  23981  cnfcf  24017  metcnp  24516  caucfil  25260  ovolgelb  25457  ismbl  25503  dyadmbllem  25576  itg2leub  25711  ellimc3  25856  mdegleb  26039  jensen  26966  dchrelbas2  27214  dchrelbas3  27215  eqcuts2  27792  onsis  28280  ons2ind  28281  nmoubi  30858  nmobndseqi  30865  nmobndseqiALT  30866  h1dei  31636  nmopub  31994  nmfnleub  32011  mdsl1i  32407  mdsl2i  32408  elat2  32426  rabsspr  32586  rabsstp  32587  islinds5  33442  islbs5  33455  eulerpartlemgvv  34536  bnj115  34884  bnj1109  34945  bnj1533  35010  bnj580  35071  bnj864  35080  bnj865  35081  bnj1049  35132  bnj1090  35137  bnj1093  35138  bnj1133  35147  bnj1171  35158  climuzcnv  35869  axextprim  35899  biimpexp  35915  dfon2lem8  35986  dffun10  36110  filnetlem4  36579  mh-unprimbi  36742  bj-substax12  37037  wl-2sb6d  37897  poimirlem25  37980  poimirlem30  37985  r2alan  38586  inxpss  38652  moantr  38707  qmapeldisjsim  39195  isat3  39767  isltrn2N  40580  cdlemefrs29bpre0  40856  cdleme32fva  40897  sn-axrep5v  42672  dford4  43475  fnwe2lem2  43497  ifpidg  43936  ifpim23g  43940  elmapintrab  44021  undmrnresiss  44049  df3or2  44213  df3an2  44214  dfhe3  44220  dffrege76  44384  dffrege115  44423  ntrneiiso  44536  ismnushort  44746  pm11.62  44839  2sbc6g  44860  expcomdg  44945  impexpd  44958  dfvd2  45024  dfvd3  45036  modelac8prim  45437  rabssf  45567  2rexsb  47561  2rexrsb  47562  snlindsntor  48959  elbigo2  49040  exp12bd  49283  ralbidb  49287  ralbidc  49288