Theorem impexp 453

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imdistan  570  pm4.14  805  nan  827  pm4.87  839  pm5.6  998  2sb6  2094  r2allem  3202  r3al  3204  r19.23t  3315  ceqsralt  3530  rspc2gv  3634  ralrab  3687  ralrab2  3692  euind  3717  reu2  3718  reu3  3720  rmo4  3723  rmo3f  3727  reuind  3746  2reu5lem3  3750  rmo2  3872  rmo3  3874  rmo3OLD  3875  rmoanim  3880  rmoanimALT  3881  ralss  4039  rabss  4050  raldifb  4123  rabsssn  4609  raldifsni  4730  unissb  4872  elintrab  4890  ssintrab  4901  dftr5  5177  axrep5  5198  reusv2lem4  5304  reusv2  5306  reusv3  5308  raliunxp  5712  fununi  6431  fvn0ssdmfun  6844  dff13  7015  ordunisuc2  7561  dfom2  7584  dfsmo2  7986  qliftfun  8384  dfsup2  8910  wemapsolem  9016  iscard2  9407  acnnum  9480  aceq1  9545  dfac9  9564  dfacacn  9569  axgroth6  10252  sstskm  10266  infm3  11602  prime  12066  raluz  12299  raluz2  12300  nnwos  12318  ralrp  12412  facwordi  13652  cotr2g  14338  rexuzre  14714  limsupgle  14836  ello12  14875  elo12  14886  lo1resb  14923  rlimresb  14924  o1resb  14925  modfsummod  15151  isprm2  16028  isprm4  16030  isprm7  16054  acsfn2  16936  pgpfac1  19204  isirred2  19453  isdomn2  20074  coe1fzgsumd  20472  evl1gsumd  20522  islindf4  20984  ist1-2  21957  isnrm2  21968  dfconn2  22029  1stccn  22073  iskgen3  22159  hausdiag  22255  cnflf  22612  txflf  22616  cnfcf  22652  metcnp  23153  caucfil  23888  ovolgelb  24083  ismbl  24129  dyadmbllem  24202  itg2leub  24337  ellimc3  24479  mdegleb  24660  jensen  25568  dchrelbas2  25815  dchrelbas3  25816  nmoubi  28551  nmobndseqi  28558  nmobndseqiALT  28559  h1dei  29329  nmopub  29687  nmfnleub  29704  mdsl1i  30100  mdsl2i  30101  elat2  30119  moel  30254  islinds5  30934  eulerpartlemgvv  31636  bnj115  31997  bnj1109  32060  bnj1533  32126  bnj580  32187  bnj864  32196  bnj865  32197  bnj1049  32248  bnj1090  32253  bnj1093  32254  bnj1133  32263  bnj1171  32274  climuzcnv  32916  axextprim  32929  biimpexp  32948  dfpo2  32993  dfon2lem8  33037  dffun10  33377  filnetlem4  33731  wl-2sb6d  34796  wl-dfrmosb  34855  wl-dfrmov  34856  wl-dfrmof  34857  poimirlem25  34919  poimirlem30  34924  inxpss  35571  moantr  35618  isat3  36445  isltrn2N  37258  cdlemefrs29bpre0  37534  cdleme32fva  37575  sn-axrep5v  39115  dford4  39633  fnwe2lem2  39658  isdomn3  39811  ifpidg  39864  ifpim23g  39868  elmapintrab  39943  undmrnresiss  39971  df3or2  40120  df3an2  40121  dfhe3  40128  dffrege76  40292  dffrege115  40331  ntrneiiso  40448  pm11.62  40733  2sbc6g  40754  expcomdg  40841  impexpd  40854  dfvd2  40920  dfvd3  40932  rabssf  41392  2rexsb  43306  2rexrsb  43307  snlindsntor  44533  elbigo2  44619