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  2089  r2allem  3120  r3al  3170  r19.23t  3228  ceqsralt  3471  rspc2gv  3587  ralrab  3653  ralrab2  3657  euind  3683  reu2  3684  reu3  3686  rmo4  3689  rmo3f  3693  reuind  3712  2reu5lem3  3716  rmo2  3838  rmo3  3840  rmoanim  3845  rmoanimALT  3846  ralss  4009  ralssOLD  4011  rabss  4022  raldifb  4099  ralin  4199  rabsssn  4621  raldifsni  4747  unissb  4891  elintrab  4910  ssintrab  4921  dftr5  5202  axrep5  5225  reusv2lem4  5339  reusv2  5341  reusv3  5343  raliunxp  5779  dfpo2  6243  fununi  6556  fvn0ssdmfun  7007  dff13  7188  ordunisuc2  7774  dfom2  7798  frpoins3xpg  8070  frpoins3xp3g  8071  xpord2indlem  8077  xpord3inddlem  8084  dfsmo2  8267  qliftfun  8726  dfsup2  9328  wemapsolem  9436  iscard2  9866  acnnum  9940  aceq1  10005  dfac9  10025  dfacacn  10030  axgroth6  10716  sstskm  10730  infm3  12078  prime  12551  raluz  12791  raluz2  12792  nnwos  12810  ralrp  12909  facwordi  14193  cotr2g  14880  rexuzre  15257  limsupgle  15381  ello12  15420  elo12  15431  lo1resb  15468  rlimresb  15469  o1resb  15470  modfsummod  15698  isprm2  16590  isprm4  16592  isprm7  16616  acsfn2  17566  pgpfac1  19992  isirred2  20337  isdomn2OLD  20625  isdomn3  20628  islindf4  21773  coe1fzgsumd  22217  evl1gsumd  22270  ist1-2  23260  isnrm2  23271  dfconn2  23332  1stccn  23376  iskgen3  23462  hausdiag  23558  cnflf  23915  txflf  23919  cnfcf  23955  metcnp  24454  caucfil  25208  ovolgelb  25406  ismbl  25452  dyadmbllem  25525  itg2leub  25660  ellimc3  25805  mdegleb  25994  jensen  26924  dchrelbas2  27173  dchrelbas3  27174  eqscut2  27745  onsis  28206  nmoubi  30747  nmobndseqi  30754  nmobndseqiALT  30755  h1dei  31525  nmopub  31883  nmfnleub  31900  mdsl1i  32296  mdsl2i  32297  elat2  32315  rabsspr  32476  rabsstp  32477  islinds5  33327  islbs5  33340  eulerpartlemgvv  34384  bnj115  34732  bnj1109  34793  bnj1533  34859  bnj580  34920  bnj864  34929  bnj865  34930  bnj1049  34981  bnj1090  34986  bnj1093  34987  bnj1133  34996  bnj1171  35007  climuzcnv  35703  axextprim  35733  biimpexp  35749  dfon2lem8  35823  dffun10  35947  filnetlem4  36414  bj-substax12  36754  wl-2sb6d  37591  poimirlem25  37684  poimirlem30  37689  r2alan  38283  inxpss  38344  moantr  38391  isat3  39345  isltrn2N  40158  cdlemefrs29bpre0  40434  cdleme32fva  40475  sn-axrep5v  42248  dford4  43061  fnwe2lem2  43083  ifpidg  43523  ifpim23g  43527  elmapintrab  43608  undmrnresiss  43636  df3or2  43800  df3an2  43801  dfhe3  43807  dffrege76  43971  dffrege115  44010  ntrneiiso  44123  ismnushort  44333  pm11.62  44426  2sbc6g  44447  expcomdg  44532  impexpd  44545  dfvd2  44611  dfvd3  44623  modelac8prim  45024  rabssf  45155  2rexsb  47131  2rexrsb  47132  snlindsntor  48502  elbigo2  48583  exp12bd  48826  ralbidb  48830  ralbidc  48831