Theorem impexp 454

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 452	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 453	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 211	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imdistan  575  pm4.14  816  nan  840  pm4.87  854  pm5.6  1014  2sb6  2118  r2allem  3149  r3al  3199  r19.23t  3257  ceqsralt  3487  rspc2gv  3591  ralrab  3656  ralrab2  3660  euind  3686  reu2  3687  reu3  3689  rmo4  3692  rmo3f  3696  reuind  3715  2reu5lem3  3719  rmo2  3840  rmo3  3842  rmoanim  3847  rmoanimALT  3848  ralss  4009  ralssOLD  4011  rabss  4023  raldifb  4102  ralin  4201  rabsssn  4626  raldifsni  4754  unissb  4898  elintrab  4917  ssintrab  4928  dftr5  5210  axrep5  5234  reusv2lem4  5357  reusv2  5359  reusv3  5361  raliunxp  5809  dfpo2  6279  fununi  6592  fvn0ssdmfun  7051  dff13  7234  ordunisuc2  7820  dfom2  7844  frpoins3xpg  8115  frpoins3xp3g  8116  xpord2indlem  8122  xpord3inddlem  8129  dfsmo2  8313  qliftfun  8779  dfsup2  9387  wemapsolem  9495  iscard2  9931  acnnum  10005  aceq1  10070  dfac9  10090  dfacacn  10095  axgroth6  10783  sstskm  10797  infm3  12148  prime  12651  raluz  12894  raluz2  12895  nnwos  12913  ralrp  13012  facwordi  14299  cotr2g  14986  rexuzre  15363  limsupgle  15487  ello12  15526  elo12  15537  lo1resb  15574  rlimresb  15575  o1resb  15576  modfsummod  15805  isprm2  16699  isprm4  16701  isprm7  16726  acsfn2  17678  pgpfac1  20105  isirred2  20449  isdomn2OLD  20741  isdomn3  20744  islindf4  21870  coe1fzgsumd  22347  evl1gsumd  22400  ist1-2  23387  isnrm2  23398  dfconn2  23459  1stccn  23503  iskgen3  23589  hausdiag  23685  cnflf  24042  txflf  24046  cnfcf  24082  metcnp  24581  caucfil  25325  ovolgelb  25522  ismbl  25568  dyadmbllem  25641  itg2leub  25776  ellimc3  25921  mdegleb  26104  jensen  27030  dchrelbas2  27278  dchrelbas3  27279  eqcuts2  27856  onsis  28344  ons2ind  28345  nmoubi  30921  nmobndseqi  30928  nmobndseqiALT  30929  h1dei  31699  nmopub  32057  nmfnleub  32074  mdsl1i  32470  mdsl2i  32471  elat2  32489  rabsspr  32649  rabsstp  32650  islinds5  33514  islbs5  33527  eulerpartlemgvv  34634  bnj115  34985  bnj1109  35046  bnj1533  35111  bnj580  35172  bnj864  35181  bnj865  35182  bnj1049  35233  bnj1090  35238  bnj1093  35239  bnj1133  35248  bnj1171  35259  climuzcnv  35985  axextprim  36015  biimpexp  36031  dfon2lem8  36102  dffun10  36226  filnetlem4  36705  mh-unprimbi  36868  bj-substax12  37163  wl-2sb6d  38025  poimirlem25  38108  poimirlem30  38113  r2alan  38714  inxpss  38780  moantr  38835  qmapeldisjsim  39323  isat3  39895  isltrn2N  40708  cdlemefrs29bpre0  40984  cdleme32fva  41025  sn-axrep5v  42800  dford4  43570  fnwe2lem2  43592  ifpidg  44031  ifpim23g  44035  elmapintrab  44116  undmrnresiss  44144  df3or2  44308  df3an2  44309  dfhe3  44315  dffrege76  44479  dffrege115  44518  ntrneiiso  44631  ismnushort  44841  pm11.62  44934  2sbc6g  44955  expcomdg  45040  impexpd  45053  dfvd2  45119  dfvd3  45131  modelac8prim  45532  rabssf  45661  2rexsb  47659  2rexrsb  47660  snlindsntor  49057  elbigo2  49138  exp12bd  49381  ralbidb  49385  ralbidc  49386