Theorem impexp 452

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imdistan  569  pm4.14  806  nan  829  pm4.87  842  pm5.6  1001  2sb6  2090  r2allem  3143  r3al  3197  r19.23t  3253  moelOLD  3402  ceqsralt  3507  rspc2gv  3622  ralrab  3690  ralrab2  3695  euind  3721  reu2  3722  reu3  3724  rmo4  3727  rmo3f  3731  reuind  3750  2reu5lem3  3754  rmo2  3882  rmo3  3884  rmoanim  3889  rmoanimALT  3890  ralss  4055  rabss  4070  raldifb  4145  rabsssn  4671  raldifsni  4799  unissb  4944  unissbOLD  4945  elintrab  4965  ssintrab  4976  dftr5  5270  dftr5OLD  5271  axrep5  5292  reusv2lem4  5400  reusv2  5402  reusv3  5404  raliunxp  5840  dfpo2  6296  fununi  6624  fvn0ssdmfun  7077  dff13  7254  ordunisuc2  7833  dfom2  7857  frpoins3xpg  8126  frpoins3xp3g  8127  xpord2indlem  8133  xpord3inddlem  8140  dfsmo2  8347  qliftfun  8796  dfsup2  9439  wemapsolem  9545  iscard2  9971  acnnum  10047  aceq1  10112  dfac9  10131  dfacacn  10136  axgroth6  10823  sstskm  10837  infm3  12173  prime  12643  raluz  12880  raluz2  12881  nnwos  12899  ralrp  12994  facwordi  14249  cotr2g  14923  rexuzre  15299  limsupgle  15421  ello12  15460  elo12  15471  lo1resb  15508  rlimresb  15509  o1resb  15510  modfsummod  15740  isprm2  16619  isprm4  16621  isprm7  16645  acsfn2  17607  pgpfac1  19950  isirred2  20235  isdomn2  20915  islindf4  21393  coe1fzgsumd  21826  evl1gsumd  21876  ist1-2  22851  isnrm2  22862  dfconn2  22923  1stccn  22967  iskgen3  23053  hausdiag  23149  cnflf  23506  txflf  23510  cnfcf  23546  metcnp  24050  caucfil  24800  ovolgelb  24997  ismbl  25043  dyadmbllem  25116  itg2leub  25252  ellimc3  25396  mdegleb  25582  jensen  26493  dchrelbas2  26740  dchrelbas3  26741  eqscut2  27308  nmoubi  30056  nmobndseqi  30063  nmobndseqiALT  30064  h1dei  30834  nmopub  31192  nmfnleub  31209  mdsl1i  31605  mdsl2i  31606  elat2  31624  islinds5  32511  islbs5  32527  eulerpartlemgvv  33406  bnj115  33767  bnj1109  33828  bnj1533  33894  bnj580  33955  bnj864  33964  bnj865  33965  bnj1049  34016  bnj1090  34021  bnj1093  34022  bnj1133  34031  bnj1171  34042  climuzcnv  34687  axextprim  34701  biimpexp  34717  dfon2lem8  34793  dffun10  34917  filnetlem4  35314  bj-substax12  35647  wl-2sb6d  36471  poimirlem25  36561  poimirlem30  36566  ralin  37163  r2alan  37164  inxpss  37228  moantr  37281  isat3  38225  isltrn2N  39039  cdlemefrs29bpre0  39315  cdleme32fva  39356  sn-axrep5v  41081  dford4  41816  fnwe2lem2  41841  isdomn3  41994  ifpidg  42290  ifpim23g  42294  elmapintrab  42375  undmrnresiss  42403  df3or2  42567  df3an2  42568  dfhe3  42574  dffrege76  42738  dffrege115  42777  ntrneiiso  42890  ismnushort  43108  pm11.62  43201  2sbc6g  43222  expcomdg  43309  impexpd  43322  dfvd2  43388  dfvd3  43400  rabssf  43856  2rexsb  45857  2rexrsb  45858  snlindsntor  47200  elbigo2  47286  exp12bd  47529  ralbidb  47533  ralbidc  47534