Theorem impexp 452

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imdistan  569  pm4.14  806  nan  829  pm4.87  842  pm5.6  1001  2sb6  2090  r2allem  3143  r3al  3197  r19.23t  3253  moelOLD  3402  ceqsralt  3507  rspc2gv  3622  ralrab  3690  ralrab2  3695  euind  3721  reu2  3722  reu3  3724  rmo4  3727  rmo3f  3731  reuind  3750  2reu5lem3  3754  rmo2  3882  rmo3  3884  rmoanim  3889  rmoanimALT  3890  ralss  4055  rabss  4070  raldifb  4145  rabsssn  4671  raldifsni  4799  unissb  4944  unissbOLD  4945  elintrab  4965  ssintrab  4976  dftr5  5270  dftr5OLD  5271  axrep5  5292  reusv2lem4  5400  reusv2  5402  reusv3  5404  raliunxp  5840  dfpo2  6296  fununi  6624  fvn0ssdmfun  7077  dff13  7254  ordunisuc2  7833  dfom2  7857  frpoins3xpg  8126  frpoins3xp3g  8127  xpord2indlem  8133  xpord3inddlem  8140  dfsmo2  8347  qliftfun  8796  dfsup2  9439  wemapsolem  9545  iscard2  9971  acnnum  10047  aceq1  10112  dfac9  10131  dfacacn  10136  axgroth6  10823  sstskm  10837  infm3  12173  prime  12643  raluz  12880  raluz2  12881  nnwos  12899  ralrp  12994  facwordi  14249  cotr2g  14923  rexuzre  15299  limsupgle  15421  ello12  15460  elo12  15471  lo1resb  15508  rlimresb  15509  o1resb  15510  modfsummod  15740  isprm2  16619  isprm4  16621  isprm7  16645  acsfn2  17607  pgpfac1  19950  isirred2  20235  isdomn2  20915  islindf4  21393  coe1fzgsumd  21826  evl1gsumd  21876  ist1-2  22851  isnrm2  22862  dfconn2  22923  1stccn  22967  iskgen3  23053  hausdiag  23149  cnflf  23506  txflf  23510  cnfcf  23546  metcnp  24050  caucfil  24800  ovolgelb  24997  ismbl  25043  dyadmbllem  25116  itg2leub  25252  ellimc3  25396  mdegleb  25582  jensen  26493  dchrelbas2  26740  dchrelbas3  26741  eqscut2  27307  nmoubi  30025  nmobndseqi  30032  nmobndseqiALT  30033  h1dei  30803  nmopub  31161  nmfnleub  31178  mdsl1i  31574  mdsl2i  31575  elat2  31593  islinds5  32480  islbs5  32496  eulerpartlemgvv  33375  bnj115  33736  bnj1109  33797  bnj1533  33863  bnj580  33924  bnj864  33933  bnj865  33934  bnj1049  33985  bnj1090  33990  bnj1093  33991  bnj1133  34000  bnj1171  34011  climuzcnv  34656  axextprim  34670  biimpexp  34686  dfon2lem8  34762  dffun10  34886  filnetlem4  35266  bj-substax12  35599  wl-2sb6d  36423  poimirlem25  36513  poimirlem30  36518  ralin  37115  r2alan  37116  inxpss  37180  moantr  37233  isat3  38177  isltrn2N  38991  cdlemefrs29bpre0  39267  cdleme32fva  39308  sn-axrep5v  41033  dford4  41768  fnwe2lem2  41793  isdomn3  41946  ifpidg  42242  ifpim23g  42246  elmapintrab  42327  undmrnresiss  42355  df3or2  42519  df3an2  42520  dfhe3  42526  dffrege76  42690  dffrege115  42729  ntrneiiso  42842  ismnushort  43060  pm11.62  43153  2sbc6g  43174  expcomdg  43261  impexpd  43274  dfvd2  43340  dfvd3  43352  rabssf  43808  2rexsb  45809  2rexrsb  45810  snlindsntor  47152  elbigo2  47238  exp12bd  47481  ralbidb  47485  ralbidc  47486