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  2091  r2allem  3121  r3al  3171  r19.23t  3229  ceqsralt  3472  rspc2gv  3583  ralrab  3649  ralrab2  3653  euind  3679  reu2  3680  reu3  3682  rmo4  3685  rmo3f  3689  reuind  3708  2reu5lem3  3712  rmo2  3834  rmo3  3836  rmoanim  3841  rmoanimALT  3842  ralss  4005  ralssOLD  4007  rabss  4019  raldifb  4098  ralin  4198  rabsssn  4620  raldifsni  4746  unissb  4891  elintrab  4910  ssintrab  4921  dftr5  5204  axrep5  5227  reusv2lem4  5341  reusv2  5343  reusv3  5345  raliunxp  5783  dfpo2  6248  fununi  6561  fvn0ssdmfun  7013  dff13  7194  ordunisuc2  7780  dfom2  7804  frpoins3xpg  8076  frpoins3xp3g  8077  xpord2indlem  8083  xpord3inddlem  8090  dfsmo2  8273  qliftfun  8732  dfsup2  9335  wemapsolem  9443  iscard2  9876  acnnum  9950  aceq1  10015  dfac9  10035  dfacacn  10040  axgroth6  10726  sstskm  10740  infm3  12088  prime  12560  raluz  12796  raluz2  12797  nnwos  12815  ralrp  12914  facwordi  14198  cotr2g  14885  rexuzre  15262  limsupgle  15386  ello12  15425  elo12  15436  lo1resb  15473  rlimresb  15474  o1resb  15475  modfsummod  15703  isprm2  16595  isprm4  16597  isprm7  16621  acsfn2  17571  pgpfac1  19996  isirred2  20341  isdomn2OLD  20629  isdomn3  20632  islindf4  21777  coe1fzgsumd  22220  evl1gsumd  22273  ist1-2  23263  isnrm2  23274  dfconn2  23335  1stccn  23379  iskgen3  23465  hausdiag  23561  cnflf  23918  txflf  23922  cnfcf  23958  metcnp  24457  caucfil  25211  ovolgelb  25409  ismbl  25455  dyadmbllem  25528  itg2leub  25663  ellimc3  25808  mdegleb  25997  jensen  26927  dchrelbas2  27176  dchrelbas3  27177  eqscut2  27748  onsis  28209  nmoubi  30754  nmobndseqi  30761  nmobndseqiALT  30762  h1dei  31532  nmopub  31890  nmfnleub  31907  mdsl1i  32303  mdsl2i  32304  elat2  32322  rabsspr  32483  rabsstp  32484  islinds5  33339  islbs5  33352  eulerpartlemgvv  34410  bnj115  34758  bnj1109  34819  bnj1533  34885  bnj580  34946  bnj864  34955  bnj865  34956  bnj1049  35007  bnj1090  35012  bnj1093  35013  bnj1133  35022  bnj1171  35033  climuzcnv  35736  axextprim  35766  biimpexp  35782  dfon2lem8  35853  dffun10  35977  filnetlem4  36446  bj-substax12  36786  wl-2sb6d  37623  poimirlem25  37705  poimirlem30  37710  r2alan  38306  inxpss  38369  moantr  38416  isat3  39426  isltrn2N  40239  cdlemefrs29bpre0  40515  cdleme32fva  40556  sn-axrep5v  42334  dford4  43146  fnwe2lem2  43168  ifpidg  43608  ifpim23g  43612  elmapintrab  43693  undmrnresiss  43721  df3or2  43885  df3an2  43886  dfhe3  43892  dffrege76  44056  dffrege115  44095  ntrneiiso  44208  ismnushort  44418  pm11.62  44511  2sbc6g  44532  expcomdg  44617  impexpd  44630  dfvd2  44696  dfvd3  44708  modelac8prim  45109  rabssf  45240  2rexsb  47225  2rexrsb  47226  snlindsntor  48596  elbigo2  48677  exp12bd  48920  ralbidb  48924  ralbidc  48925