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  843  pm5.6  1003  2sb6  2083  r2allem  3139  r3al  3194  r19.23t  3252  moelOLD  3402  ceqsralt  3513  rspc2gv  3631  ralrab  3701  ralrab2  3706  euind  3732  reu2  3733  reu3  3735  rmo4  3738  rmo3f  3742  reuind  3761  2reu5lem3  3765  rmo2  3895  rmo3  3897  rmoanim  3902  rmoanimALT  3903  ralss  4069  rabss  4081  raldifb  4158  rabsssn  4672  raldifsni  4799  unissb  4943  unissbOLD  4944  elintrab  4964  ssintrab  4975  dftr5  5268  dftr5OLD  5269  axrep5  5292  reusv2lem4  5406  reusv2  5408  reusv3  5410  raliunxp  5852  dfpo2  6317  fununi  6642  fvn0ssdmfun  7093  dff13  7274  ordunisuc2  7864  dfom2  7888  frpoins3xpg  8163  frpoins3xp3g  8164  xpord2indlem  8170  xpord3inddlem  8177  dfsmo2  8385  qliftfun  8840  dfsup2  9481  wemapsolem  9587  iscard2  10013  acnnum  10089  aceq1  10154  dfac9  10174  dfacacn  10179  axgroth6  10865  sstskm  10879  infm3  12224  prime  12696  raluz  12935  raluz2  12936  nnwos  12954  ralrp  13052  facwordi  14324  cotr2g  15011  rexuzre  15387  limsupgle  15509  ello12  15548  elo12  15559  lo1resb  15596  rlimresb  15597  o1resb  15598  modfsummod  15826  isprm2  16715  isprm4  16717  isprm7  16741  acsfn2  17707  pgpfac1  20114  isirred2  20437  isdomn2OLD  20728  isdomn3  20731  islindf4  21875  coe1fzgsumd  22323  evl1gsumd  22376  ist1-2  23370  isnrm2  23381  dfconn2  23442  1stccn  23486  iskgen3  23572  hausdiag  23668  cnflf  24025  txflf  24029  cnfcf  24065  metcnp  24569  caucfil  25330  ovolgelb  25528  ismbl  25574  dyadmbllem  25647  itg2leub  25783  ellimc3  25928  mdegleb  26117  jensen  27046  dchrelbas2  27295  dchrelbas3  27296  eqscut2  27865  nmoubi  30800  nmobndseqi  30807  nmobndseqiALT  30808  h1dei  31578  nmopub  31936  nmfnleub  31953  mdsl1i  32349  mdsl2i  32350  elat2  32368  rabsspr  32528  rabsstp  32529  islinds5  33374  islbs5  33387  eulerpartlemgvv  34357  bnj115  34717  bnj1109  34778  bnj1533  34844  bnj580  34905  bnj864  34914  bnj865  34915  bnj1049  34966  bnj1090  34971  bnj1093  34972  bnj1133  34981  bnj1171  34992  climuzcnv  35655  axextprim  35680  biimpexp  35696  dfon2lem8  35771  dffun10  35895  filnetlem4  36363  bj-substax12  36703  wl-2sb6d  37538  poimirlem25  37631  poimirlem30  37636  ralin  38229  r2alan  38230  inxpss  38292  moantr  38345  isat3  39288  isltrn2N  40102  cdlemefrs29bpre0  40378  cdleme32fva  40419  sn-axrep5v  42233  dford4  43017  fnwe2lem2  43039  ifpidg  43480  ifpim23g  43484  elmapintrab  43565  undmrnresiss  43593  df3or2  43757  df3an2  43758  dfhe3  43764  dffrege76  43928  dffrege115  43967  ntrneiiso  44080  ismnushort  44296  pm11.62  44389  2sbc6g  44410  expcomdg  44497  impexpd  44510  dfvd2  44576  dfvd3  44588  rabssf  45058  2rexsb  47050  2rexrsb  47051  snlindsntor  48316  elbigo2  48401  exp12bd  48644  ralbidb  48648  ralbidc  48649