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  2122  r2allem  3150  r3al  3200  r19.23t  3258  ceqsralt  3484  rspc2gv  3585  ralrab  3651  ralrab2  3655  euind  3681  reu2  3682  reu3  3684  rmo4  3687  rmo3f  3691  reuind  3710  2reu5lem3  3714  rmo2  3833  rmo3  3835  rmoanim  3841  rmoanimALT  3842  ralss  3981  ralssOLD  3983  rabss  3995  raldifb  4085  ralin  4146  rabsssn  4625  raldifsni  4754  unissb  4900  elintrab  4919  ssintrab  4930  dftr5  5215  axrep5  5238  reusv2lem4  5362  reusv2  5364  reusv3  5366  raliunxp  5815  dfpo2  6299  fununi  6616  fvn0ssdmfun  7075  dff13  7259  ordunisuc2  7856  dfom2  7880  fnwe2lem3  8150  frpoins3xpg  8160  frpoins3xp3g  8161  xpord2indlem  8167  xpord3inddlem  8174  dfsmo2  8359  qliftfun  8827  dfsup2  9440  wemapsolem  9548  iscard2  10061  acnnum  10135  aceq1  10200  dfac9  10219  dfacacn  10224  axgroth6  10917  sstskm  10931  infm3  12280  prime  12784  raluz  13027  raluz2  13028  nnwos  13046  ralrp  13146  facwordi  14437  cotr2g  15135  rexuzre  15526  limsupgle  15650  ello12  15689  elo12  15700  lo1resb  15737  rlimresb  15738  o1resb  15739  modfsummod  15967  isprm2  16863  isprm4  16865  isprm7  16890  acsfn2  17843  pgpfac1  20302  isirred2  20657  isdomn3  20972  islindf4  22150  coe1fzgsumd  22628  evl1gsumd  22681  ist1-2  23671  isnrm2  23682  dfconn2  23743  1stccn  23788  iskgen3  23874  hausdiag  23970  cnflf  24327  txflf  24331  cnfcf  24367  metcnp  24866  caucfil  25610  ovolgelb  25807  ismbl  25853  dyadmbllem  25926  itg2leub  26061  ellimc3  26205  mdegleb  26388  jensen  27322  dchrelbas2  27570  dchrelbas3  27571  eqcuts2  28178  onsis  28666  ons2ind  28667  nmoubi  31380  nmobndseqi  31387  nmobndseqiALT  31388  h1dei  32158  nmopub  32516  nmfnleub  32533  mdsl1i  32929  mdsl2i  32930  elat2  32948  rabsspr  33145  rabsstp  33146  islinds5  33970  islbs5  33982  eulerpartlemgvv  35055  bnj115  35403  bnj1109  35464  bnj1533  35529  bnj580  35590  bnj864  35599  bnj865  35600  bnj1049  35651  bnj1090  35656  bnj1093  35657  bnj1133  35666  bnj1171  35677  climuzcnv  36523  axextprim  36559  biimpexp  36575  dfon2lem8  36645  dffun10  36769  filnetlem4  37262  mh-unprimbi  37425  bj-substax12  37719  wl-2sb6d  38584  poimirlem25  38657  poimirlem30  38662  r2alan  39277  inxpss  39343  moantr  39398  qmapeldisjsim  39886  isat3  40458  isltrn2N  41271  cdlemefrs29bpre0  41547  cdleme32fva  41588  sn-axrep5v  43365  dford4  44130  ifpidg  44586  ifpim23g  44590  elmapintrab  44671  undmrnresiss  44698  df3or2  44862  df3an2  44863  dfhe3  44869  dffrege76  45033  dffrege115  45072  ntrneiiso  45185  ismnushort  45379  pm11.62  45472  2sbc6g  45493  expcomdg  45577  impexpd  45590  dfvd2  45656  dfvd3  45668  modelac8prim  46076  rabssf  46228  2rexsb  48265  2rexrsb  48266  snlindsntor  49677  elbigo2  49758  exp12bd  50000  ralbidb  50004  ralbidc  50005  dfrals2  51055  dfralseu2  51088