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  2087  r2allem  3122  r3al  3176  r19.23t  3234  ceqsralt  3485  rspc2gv  3601  ralrab  3668  ralrab2  3672  euind  3698  reu2  3699  reu3  3701  rmo4  3704  rmo3f  3708  reuind  3727  2reu5lem3  3731  rmo2  3853  rmo3  3855  rmoanim  3860  rmoanimALT  3861  ralss  4024  ralssOLD  4026  rabss  4038  raldifb  4115  ralin  4215  rabsssn  4635  raldifsni  4762  unissb  4906  unissbOLD  4907  elintrab  4927  ssintrab  4938  dftr5  5221  dftr5OLD  5222  axrep5  5245  reusv2lem4  5359  reusv2  5361  reusv3  5363  raliunxp  5806  dfpo2  6272  fununi  6594  fvn0ssdmfun  7049  dff13  7232  ordunisuc2  7823  dfom2  7847  frpoins3xpg  8122  frpoins3xp3g  8123  xpord2indlem  8129  xpord3inddlem  8136  dfsmo2  8319  qliftfun  8778  dfsup2  9402  wemapsolem  9510  iscard2  9936  acnnum  10012  aceq1  10077  dfac9  10097  dfacacn  10102  axgroth6  10788  sstskm  10802  infm3  12149  prime  12622  raluz  12862  raluz2  12863  nnwos  12881  ralrp  12980  facwordi  14261  cotr2g  14949  rexuzre  15326  limsupgle  15450  ello12  15489  elo12  15500  lo1resb  15537  rlimresb  15538  o1resb  15539  modfsummod  15767  isprm2  16659  isprm4  16661  isprm7  16685  acsfn2  17631  pgpfac1  20019  isirred2  20337  isdomn2OLD  20628  isdomn3  20631  islindf4  21754  coe1fzgsumd  22198  evl1gsumd  22251  ist1-2  23241  isnrm2  23252  dfconn2  23313  1stccn  23357  iskgen3  23443  hausdiag  23539  cnflf  23896  txflf  23900  cnfcf  23936  metcnp  24436  caucfil  25190  ovolgelb  25388  ismbl  25434  dyadmbllem  25507  itg2leub  25642  ellimc3  25787  mdegleb  25976  jensen  26906  dchrelbas2  27155  dchrelbas3  27156  eqscut2  27725  onsis  28179  nmoubi  30708  nmobndseqi  30715  nmobndseqiALT  30716  h1dei  31486  nmopub  31844  nmfnleub  31861  mdsl1i  32257  mdsl2i  32258  elat2  32276  rabsspr  32437  rabsstp  32438  islinds5  33345  islbs5  33358  eulerpartlemgvv  34374  bnj115  34722  bnj1109  34783  bnj1533  34849  bnj580  34910  bnj864  34919  bnj865  34920  bnj1049  34971  bnj1090  34976  bnj1093  34977  bnj1133  34986  bnj1171  34997  climuzcnv  35665  axextprim  35695  biimpexp  35711  dfon2lem8  35785  dffun10  35909  filnetlem4  36376  bj-substax12  36716  wl-2sb6d  37553  poimirlem25  37646  poimirlem30  37651  r2alan  38245  inxpss  38306  moantr  38353  isat3  39307  isltrn2N  40121  cdlemefrs29bpre0  40397  cdleme32fva  40438  sn-axrep5v  42211  dford4  43025  fnwe2lem2  43047  ifpidg  43487  ifpim23g  43491  elmapintrab  43572  undmrnresiss  43600  df3or2  43764  df3an2  43765  dfhe3  43771  dffrege76  43935  dffrege115  43974  ntrneiiso  44087  ismnushort  44297  pm11.62  44390  2sbc6g  44411  expcomdg  44497  impexpd  44510  dfvd2  44576  dfvd3  44588  modelac8prim  44989  rabssf  45120  2rexsb  47106  2rexrsb  47107  snlindsntor  48464  elbigo2  48545  exp12bd  48788  ralbidb  48792  ralbidc  48793