Theorem impexp 461

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm4.14  601  nan  603  pm4.87  607  imp4aOLD  614  exp4aOLD  633  imdistan  725  pm5.3  748  pm5.6  971  2sb6  2472  r2allem  2966  r3al  2969  r19.23t  3050  ceqsralt  3260  rspc2gv  3352  ralrab  3401  ralrab2  3405  euind  3426  reu2  3427  reu3  3429  rmo4  3432  reuind  3444  2reu5lem3  3448  rmo2  3559  rmo3  3561  ralss  3701  rabss  3712  raldifb  3783  rabsssn  4247  raldifsni  4357  unissb  4501  elintrab  4520  ssintrab  4532  dftr5  4788  axrep5  4809  reusv2lem4  4902  reusv2  4904  reusv3  4906  raliunxp  5294  fununi  6002  fvn0ssdmfun  6390  dff13  6552  ordunisuc2  7086  dfom2  7109  dfsmo2  7489  qliftfun  7875  dfsup2  8391  wemapsolem  8496  iscard2  8840  acnnum  8913  aceq1  8978  dfac9  8996  dfacacn  9001  axgroth6  9688  sstskm  9702  infm3  11020  prime  11496  raluz  11774  raluz2  11775  nnwos  11793  ralrp  11890  facwordi  13116  cotr2g  13761  rexuzre  14136  limsupgle  14252  ello12  14291  elo12  14302  lo1resb  14339  rlimresb  14340  o1resb  14341  modfsummod  14570  isprm2  15442  isprm4  15444  isprm7  15467  acsfn2  16371  pgpfac1  18525  isirred2  18747  isdomn2  19347  coe1fzgsumd  19720  evl1gsumd  19769  islindf4  20225  ist1-2  21199  isnrm2  21210  dfconn2  21270  1stccn  21314  iskgen3  21400  hausdiag  21496  cnflf  21853  txflf  21857  cnfcf  21893  metcnp  22393  caucfil  23127  ovolgelb  23294  ismbl  23340  dyadmbllem  23413  itg2leub  23546  ellimc3  23688  mdegleb  23869  jensen  24760  dchrelbas2  25007  dchrelbas3  25008  nmoubi  27755  nmobndseqi  27762  nmobndseqiALT  27763  h1dei  28537  nmopub  28895  nmfnleub  28912  mdsl1i  29308  mdsl2i  29309  elat2  29327  moel  29451  rmo3f  29462  rmo4fOLD  29463  eulerpartlemgvv  30566  bnj115  30919  bnj1109  30983  bnj1533  31048  bnj580  31109  bnj864  31118  bnj865  31119  bnj1049  31168  bnj1090  31173  bnj1093  31174  bnj1133  31183  bnj1171  31194  climuzcnv  31691  axextprim  31704  biimpexp  31723  dfpo2  31771  dfon2lem8  31819  dffun10  32146  filnetlem4  32501  bj-axrep5  32917  wl-2sb6d  33471  poimirlem25  33564  poimirlem30  33569  inxpss  34223  moantr  34267  isat3  34912  isltrn2N  35724  cdlemefrs29bpre0  36001  cdleme32fva  36042  dford4  37913  fnwe2lem2  37938  isdomn3  38099  ifpidg  38153  ifpim23g  38157  elmapintrab  38199  undmrnresiss  38227  df3or2  38377  df3an2  38378  dfhe3  38386  dffrege76  38550  dffrege115  38589  ntrneiiso  38706  pm11.62  38911  2sbc6g  38933  expcomdg  39023  impexpd  39036  dfvd2  39112  dfvd3  39124  rabssf  39616  2rexsb  41491  2rexrsb  41492  rmoanim  41500  snlindsntor  42585  elbigo2  42671