Theorem impexp 456

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imdistan  578  pm4.14  819  nan  843  pm4.87  857  pm5.6  1017  2sb6  2123  r2allem  3151  r3al  3201  r19.23t  3259  ceqsralt  3485  rspc2gv  3586  ralrab  3652  ralrab2  3656  euind  3682  reu2  3683  reu3  3685  rmo4  3688  rmo3f  3692  reuind  3711  2reu5lem3  3715  rmo2  3834  rmo3  3836  rmoanim  3842  rmoanimALT  3843  ralss  4004  ralssOLD  4006  rabss  4018  raldifb  4096  ralin  4195  rabsssn  4629  raldifsni  4758  unissb  4901  elintrab  4920  ssintrab  4931  dftr5  5216  axrep5  5239  reusv2lem4  5363  reusv2  5365  reusv3  5367  raliunxp  5816  dfpo2  6298  fununi  6613  fvn0ssdmfun  7072  dff13  7256  ordunisuc2  7853  dfom2  7877  frpoins3xpg  8150  frpoins3xp3g  8151  xpord2indlem  8157  xpord3inddlem  8164  dfsmo2  8348  qliftfun  8816  dfsup2  9429  wemapsolem  9537  iscard2  10050  acnnum  10124  aceq1  10189  dfac9  10208  dfacacn  10213  axgroth6  10906  sstskm  10920  infm3  12269  prime  12773  raluz  13016  raluz2  13017  nnwos  13035  ralrp  13135  facwordi  14426  cotr2g  15122  rexuzre  15513  limsupgle  15637  ello12  15676  elo12  15687  lo1resb  15724  rlimresb  15725  o1resb  15726  modfsummod  15954  isprm2  16850  isprm4  16852  isprm7  16877  acsfn2  17830  pgpfac1  20289  isirred2  20644  isdomn3  20959  islindf4  22137  coe1fzgsumd  22615  evl1gsumd  22668  ist1-2  23658  isnrm2  23669  dfconn2  23730  1stccn  23775  iskgen3  23861  hausdiag  23957  cnflf  24314  txflf  24318  cnfcf  24354  metcnp  24853  caucfil  25597  ovolgelb  25794  ismbl  25840  dyadmbllem  25913  itg2leub  26048  ellimc3  26192  mdegleb  26375  jensen  27309  dchrelbas2  27557  dchrelbas3  27558  eqcuts2  28165  onsis  28653  ons2ind  28654  nmoubi  31367  nmobndseqi  31374  nmobndseqiALT  31375  h1dei  32145  nmopub  32503  nmfnleub  32520  mdsl1i  32916  mdsl2i  32917  elat2  32935  rabsspr  33090  rabsstp  33091  islinds5  33916  islbs5  33928  eulerpartlemgvv  35001  bnj115  35349  bnj1109  35410  bnj1533  35475  bnj580  35536  bnj864  35545  bnj865  35546  bnj1049  35597  bnj1090  35602  bnj1093  35603  bnj1133  35612  bnj1171  35623  climuzcnv  36415  axextprim  36445  biimpexp  36461  dfon2lem8  36532  dffun10  36656  filnetlem4  37149  mh-unprimbi  37312  bj-substax12  37606  wl-2sb6d  38470  poimirlem25  38543  poimirlem30  38548  r2alan  39163  inxpss  39229  moantr  39284  qmapeldisjsim  39772  isat3  40344  isltrn2N  41157  cdlemefrs29bpre0  41433  cdleme32fva  41474  sn-axrep5v  43251  dford4  44015  fnwe2lem2  44037  ifpidg  44476  ifpim23g  44480  elmapintrab  44561  undmrnresiss  44589  df3or2  44753  df3an2  44754  dfhe3  44760  dffrege76  44924  dffrege115  44963  ntrneiiso  45076  ismnushort  45270  pm11.62  45363  2sbc6g  45384  expcomdg  45468  impexpd  45481  dfvd2  45547  dfvd3  45559  modelac8prim  45960  rabssf  46103  2rexsb  48140  2rexrsb  48141  snlindsntor  49552  elbigo2  49633  exp12bd  49875  ralbidb  49879  ralbidc  49880  dfrals2  50855  dfralseu2  50888