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  3121  r3al  3175  r19.23t  3233  ceqsralt  3482  rspc2gv  3598  ralrab  3665  ralrab2  3669  euind  3695  reu2  3696  reu3  3698  rmo4  3701  rmo3f  3705  reuind  3724  2reu5lem3  3728  rmo2  3850  rmo3  3852  rmoanim  3857  rmoanimALT  3858  ralss  4021  ralssOLD  4023  rabss  4035  raldifb  4112  ralin  4212  rabsssn  4632  raldifsni  4759  unissb  4903  unissbOLD  4904  elintrab  4924  ssintrab  4935  dftr5  5218  dftr5OLD  5219  axrep5  5242  reusv2lem4  5356  reusv2  5358  reusv3  5360  raliunxp  5803  dfpo2  6269  fununi  6591  fvn0ssdmfun  7046  dff13  7229  ordunisuc2  7820  dfom2  7844  frpoins3xpg  8119  frpoins3xp3g  8120  xpord2indlem  8126  xpord3inddlem  8133  dfsmo2  8316  qliftfun  8775  dfsup2  9395  wemapsolem  9503  iscard2  9929  acnnum  10005  aceq1  10070  dfac9  10090  dfacacn  10095  axgroth6  10781  sstskm  10795  infm3  12142  prime  12615  raluz  12855  raluz2  12856  nnwos  12874  ralrp  12973  facwordi  14254  cotr2g  14942  rexuzre  15319  limsupgle  15443  ello12  15482  elo12  15493  lo1resb  15530  rlimresb  15531  o1resb  15532  modfsummod  15760  isprm2  16652  isprm4  16654  isprm7  16678  acsfn2  17624  pgpfac1  20012  isirred2  20330  isdomn2OLD  20621  isdomn3  20624  islindf4  21747  coe1fzgsumd  22191  evl1gsumd  22244  ist1-2  23234  isnrm2  23245  dfconn2  23306  1stccn  23350  iskgen3  23436  hausdiag  23532  cnflf  23889  txflf  23893  cnfcf  23929  metcnp  24429  caucfil  25183  ovolgelb  25381  ismbl  25427  dyadmbllem  25500  itg2leub  25635  ellimc3  25780  mdegleb  25969  jensen  26899  dchrelbas2  27148  dchrelbas3  27149  eqscut2  27718  onsis  28172  nmoubi  30701  nmobndseqi  30708  nmobndseqiALT  30709  h1dei  31479  nmopub  31837  nmfnleub  31854  mdsl1i  32250  mdsl2i  32251  elat2  32269  rabsspr  32430  rabsstp  32431  islinds5  33338  islbs5  33351  eulerpartlemgvv  34367  bnj115  34715  bnj1109  34776  bnj1533  34842  bnj580  34903  bnj864  34912  bnj865  34913  bnj1049  34964  bnj1090  34969  bnj1093  34970  bnj1133  34979  bnj1171  34990  climuzcnv  35658  axextprim  35688  biimpexp  35704  dfon2lem8  35778  dffun10  35902  filnetlem4  36369  bj-substax12  36709  wl-2sb6d  37546  poimirlem25  37639  poimirlem30  37644  r2alan  38238  inxpss  38299  moantr  38346  isat3  39300  isltrn2N  40114  cdlemefrs29bpre0  40390  cdleme32fva  40431  sn-axrep5v  42204  dford4  43018  fnwe2lem2  43040  ifpidg  43480  ifpim23g  43484  elmapintrab  43565  undmrnresiss  43593  df3or2  43757  df3an2  43758  dfhe3  43764  dffrege76  43928  dffrege115  43967  ntrneiiso  44080  ismnushort  44290  pm11.62  44383  2sbc6g  44404  expcomdg  44490  impexpd  44503  dfvd2  44569  dfvd3  44581  modelac8prim  44982  rabssf  45113  2rexsb  47102  2rexrsb  47103  snlindsntor  48460  elbigo2  48541  exp12bd  48784  ralbidb  48788  ralbidc  48789