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  2086  r2allem  3128  r3al  3182  r19.23t  3238  moelOLD  3384  ceqsralt  3495  rspc2gv  3611  ralrab  3677  ralrab2  3681  euind  3707  reu2  3708  reu3  3710  rmo4  3713  rmo3f  3717  reuind  3736  2reu5lem3  3740  rmo2  3862  rmo3  3864  rmoanim  3869  rmoanimALT  3870  ralss  4033  ralssOLD  4035  rabss  4047  raldifb  4124  ralin  4224  rabsssn  4644  raldifsni  4771  unissb  4915  unissbOLD  4916  elintrab  4936  ssintrab  4947  dftr5  5233  dftr5OLD  5234  axrep5  5257  reusv2lem4  5371  reusv2  5373  reusv3  5375  raliunxp  5819  dfpo2  6285  fununi  6610  fvn0ssdmfun  7063  dff13  7246  ordunisuc2  7837  dfom2  7861  frpoins3xpg  8137  frpoins3xp3g  8138  xpord2indlem  8144  xpord3inddlem  8151  dfsmo2  8359  qliftfun  8814  dfsup2  9454  wemapsolem  9562  iscard2  9988  acnnum  10064  aceq1  10129  dfac9  10149  dfacacn  10154  axgroth6  10840  sstskm  10854  infm3  12199  prime  12672  raluz  12910  raluz2  12911  nnwos  12929  ralrp  13027  facwordi  14305  cotr2g  14993  rexuzre  15369  limsupgle  15491  ello12  15530  elo12  15541  lo1resb  15578  rlimresb  15579  o1resb  15580  modfsummod  15808  isprm2  16699  isprm4  16701  isprm7  16725  acsfn2  17673  pgpfac1  20061  isirred2  20379  isdomn2OLD  20670  isdomn3  20673  islindf4  21796  coe1fzgsumd  22240  evl1gsumd  22293  ist1-2  23283  isnrm2  23294  dfconn2  23355  1stccn  23399  iskgen3  23485  hausdiag  23581  cnflf  23938  txflf  23942  cnfcf  23978  metcnp  24478  caucfil  25233  ovolgelb  25431  ismbl  25477  dyadmbllem  25550  itg2leub  25685  ellimc3  25830  mdegleb  26019  jensen  26949  dchrelbas2  27198  dchrelbas3  27199  eqscut2  27768  nmoubi  30699  nmobndseqi  30706  nmobndseqiALT  30707  h1dei  31477  nmopub  31835  nmfnleub  31852  mdsl1i  32248  mdsl2i  32249  elat2  32267  rabsspr  32428  rabsstp  32429  islinds5  33328  islbs5  33341  eulerpartlemgvv  34354  bnj115  34702  bnj1109  34763  bnj1533  34829  bnj580  34890  bnj864  34899  bnj865  34900  bnj1049  34951  bnj1090  34956  bnj1093  34957  bnj1133  34966  bnj1171  34977  climuzcnv  35639  axextprim  35664  biimpexp  35680  dfon2lem8  35754  dffun10  35878  filnetlem4  36345  bj-substax12  36685  wl-2sb6d  37522  poimirlem25  37615  poimirlem30  37620  r2alan  38213  inxpss  38275  moantr  38328  isat3  39271  isltrn2N  40085  cdlemefrs29bpre0  40361  cdleme32fva  40402  sn-axrep5v  42213  dford4  43000  fnwe2lem2  43022  ifpidg  43462  ifpim23g  43466  elmapintrab  43547  undmrnresiss  43575  df3or2  43739  df3an2  43740  dfhe3  43746  dffrege76  43910  dffrege115  43949  ntrneiiso  44062  ismnushort  44273  pm11.62  44366  2sbc6g  44387  expcomdg  44473  impexpd  44486  dfvd2  44552  dfvd3  44564  modelac8prim  44965  rabssf  45091  2rexsb  47078  2rexrsb  47079  snlindsntor  48395  elbigo2  48480  exp12bd  48723  ralbidb  48727  ralbidc  48728