Theorem impexp 455

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imdistan  577  pm4.14  818  nan  842  pm4.87  856  pm5.6  1017  2sb6  2122  r2allem  3153  r3al  3203  r19.23t  3261  ceqsralt  3491  rspc2gv  3594  ralrab  3660  ralrab2  3664  euind  3690  reu2  3691  reu3  3693  rmo4  3696  rmo3f  3700  reuind  3719  2reu5lem3  3723  rmo2  3843  rmo3  3845  rmoanim  3850  rmoanimALT  3851  ralss  4012  ralssOLD  4014  rabss  4026  raldifb  4105  ralin  4204  rabsssn  4630  raldifsni  4758  unissb  4902  elintrab  4921  ssintrab  4932  dftr5  5216  axrep5  5240  reusv2lem4  5363  reusv2  5365  reusv3  5367  raliunxp  5816  dfpo2  6287  fununi  6600  fvn0ssdmfun  7059  dff13  7242  ordunisuc2  7828  dfom2  7852  frpoins3xpg  8124  frpoins3xp3g  8125  xpord2indlem  8131  xpord3inddlem  8138  dfsmo2  8322  qliftfun  8788  dfsup2  9392  wemapsolem  9500  iscard2  9950  acnnum  10024  aceq1  10089  dfac9  10108  dfacacn  10113  axgroth6  10801  sstskm  10815  infm3  12165  prime  12668  raluz  12911  raluz2  12912  nnwos  12930  ralrp  13029  facwordi  14316  cotr2g  15003  rexuzre  15394  limsupgle  15518  ello12  15557  elo12  15568  lo1resb  15605  rlimresb  15606  o1resb  15607  modfsummod  15836  isprm2  16730  isprm4  16732  isprm7  16757  acsfn2  17709  pgpfac1  20143  isirred2  20494  isdomn3  20790  islindf4  21948  coe1fzgsumd  22425  evl1gsumd  22478  ist1-2  23465  isnrm2  23476  dfconn2  23537  1stccn  23581  iskgen3  23667  hausdiag  23763  cnflf  24120  txflf  24124  cnfcf  24160  metcnp  24659  caucfil  25403  ovolgelb  25600  ismbl  25646  dyadmbllem  25719  itg2leub  25854  ellimc3  25999  mdegleb  26182  jensen  27111  dchrelbas2  27359  dchrelbas3  27360  eqcuts2  27937  onsis  28425  ons2ind  28426  nmoubi  31033  nmobndseqi  31040  nmobndseqiALT  31041  h1dei  31811  nmopub  32169  nmfnleub  32186  mdsl1i  32582  mdsl2i  32583  elat2  32601  rabsspr  32757  rabsstp  32758  islinds5  33597  islbs5  33609  eulerpartlemgvv  34683  bnj115  35031  bnj1109  35092  bnj1533  35157  bnj580  35218  bnj864  35227  bnj865  35228  bnj1049  35279  bnj1090  35284  bnj1093  35285  bnj1133  35294  bnj1171  35305  climuzcnv  36034  axextprim  36064  biimpexp  36080  dfon2lem8  36151  dffun10  36275  filnetlem4  36754  mh-unprimbi  36917  bj-substax12  37211  wl-2sb6d  38073  poimirlem25  38156  poimirlem30  38161  r2alan  38762  inxpss  38828  moantr  38883  qmapeldisjsim  39371  isat3  39943  isltrn2N  40756  cdlemefrs29bpre0  41032  cdleme32fva  41073  sn-axrep5v  42848  dford4  43618  fnwe2lem2  43640  ifpidg  44079  ifpim23g  44083  elmapintrab  44164  undmrnresiss  44192  df3or2  44356  df3an2  44357  dfhe3  44363  dffrege76  44527  dffrege115  44566  ntrneiiso  44679  ismnushort  44875  pm11.62  44968  2sbc6g  44989  expcomdg  45074  impexpd  45087  dfvd2  45153  dfvd3  45165  modelac8prim  45566  rabssf  45695  2rexsb  47693  2rexrsb  47694  snlindsntor  49102  elbigo2  49183  exp12bd  49425  ralbidb  49429  ralbidc  49430