Theorem impexp 456

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imdistan  578  pm4.14  819  nan  843  pm4.87  857  pm5.6  1017  2sb6  2123  r2allem  3156  r3al  3206  r19.23t  3264  ceqsralt  3492  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  3851  rmoanimALT  3852  ralss  4013  ralssOLD  4015  rabss  4027  raldifb  4106  ralin  4205  rabsssn  4639  raldifsni  4768  unissb  4911  elintrab  4930  ssintrab  4941  dftr5  5227  axrep5  5251  reusv2lem4  5377  reusv2  5379  reusv3  5381  raliunxp  5830  dfpo2  6304  fununi  6618  fvn0ssdmfun  7076  dff13  7259  ordunisuc2  7849  dfom2  7873  frpoins3xpg  8145  frpoins3xp3g  8146  xpord2indlem  8152  xpord3inddlem  8159  dfsmo2  8343  qliftfun  8809  dfsup2  9414  wemapsolem  9522  iscard2  9981  acnnum  10055  aceq1  10120  dfac9  10139  dfacacn  10144  axgroth6  10831  sstskm  10845  infm3  12192  prime  12695  raluz  12938  raluz2  12939  nnwos  12957  ralrp  13056  facwordi  14345  cotr2g  15039  rexuzre  15430  limsupgle  15554  ello12  15593  elo12  15604  lo1resb  15641  rlimresb  15642  o1resb  15643  modfsummod  15872  isprm2  16765  isprm4  16767  isprm7  16792  acsfn2  17744  pgpfac1  20183  isirred2  20536  isdomn3  20850  islindf4  22025  coe1fzgsumd  22501  evl1gsumd  22554  ist1-2  23541  isnrm2  23552  dfconn2  23613  1stccn  23657  iskgen3  23743  hausdiag  23839  cnflf  24196  txflf  24200  cnfcf  24236  metcnp  24735  caucfil  25479  ovolgelb  25676  ismbl  25722  dyadmbllem  25795  itg2leub  25930  ellimc3  26075  mdegleb  26258  jensen  27190  dchrelbas2  27438  dchrelbas3  27439  eqcuts2  28016  onsis  28504  ons2ind  28505  nmoubi  31161  nmobndseqi  31168  nmobndseqiALT  31169  h1dei  31939  nmopub  32297  nmfnleub  32314  mdsl1i  32710  mdsl2i  32711  elat2  32729  rabsspr  32884  rabsstp  32885  islinds5  33713  islbs5  33724  eulerpartlemgvv  34798  bnj115  35146  bnj1109  35207  bnj1533  35272  bnj580  35333  bnj864  35342  bnj865  35343  bnj1049  35394  bnj1090  35399  bnj1093  35400  bnj1133  35409  bnj1171  35420  climuzcnv  36184  axextprim  36214  biimpexp  36230  dfon2lem8  36301  dffun10  36425  filnetlem4  36933  mh-unprimbi  37096  bj-substax12  37390  wl-2sb6d  38254  poimirlem25  38337  poimirlem30  38342  r2alan  38941  inxpss  39007  moantr  39062  qmapeldisjsim  39550  isat3  40122  isltrn2N  40935  cdlemefrs29bpre0  41211  cdleme32fva  41252  sn-axrep5v  43029  dford4  43797  fnwe2lem2  43819  ifpidg  44258  ifpim23g  44262  elmapintrab  44343  undmrnresiss  44371  df3or2  44535  df3an2  44536  dfhe3  44542  dffrege76  44706  dffrege115  44745  ntrneiiso  44858  ismnushort  45052  pm11.62  45145  2sbc6g  45166  expcomdg  45250  impexpd  45263  dfvd2  45329  dfvd3  45341  modelac8prim  45742  rabssf  45878  2rexsb  47879  2rexrsb  47880  snlindsntor  49292  elbigo2  49373  exp12bd  49615  ralbidb  49619  ralbidc  49620  dfrals2  50609  dfralseu2  50642