Theorem impexp 449

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

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

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 395

This theorem is referenced by:  imdistan  566  pm4.14  805  nan  828  pm4.87  841  pm5.6  999  2sb6  2082  r2allem  3132  r3al  3187  r19.23t  3243  moelOLD  3389  ceqsralt  3497  rspc2gv  3618  ralrab  3687  ralrab2  3692  euind  3718  reu2  3719  reu3  3721  rmo4  3724  rmo3f  3728  reuind  3747  2reu5lem3  3751  rmo2  3880  rmo3  3882  rmoanim  3887  rmoanimALT  3888  ralss  4054  rabss  4068  raldifb  4144  rabsssn  4675  raldifsni  4804  unissb  4947  unissbOLD  4948  elintrab  4968  ssintrab  4979  dftr5  5274  dftr5OLD  5275  axrep5  5296  reusv2lem4  5405  reusv2  5407  reusv3  5409  raliunxp  5846  dfpo2  6307  fununi  6634  fvn0ssdmfun  7088  dff13  7270  ordunisuc2  7854  dfom2  7878  frpoins3xpg  8154  frpoins3xp3g  8155  xpord2indlem  8161  xpord3inddlem  8168  dfsmo2  8377  qliftfun  8831  dfsup2  9487  wemapsolem  9593  iscard2  10019  acnnum  10095  aceq1  10160  dfac9  10179  dfacacn  10184  axgroth6  10871  sstskm  10885  infm3  12225  prime  12695  raluz  12932  raluz2  12933  nnwos  12951  ralrp  13048  facwordi  14306  cotr2g  14981  rexuzre  15357  limsupgle  15479  ello12  15518  elo12  15529  lo1resb  15566  rlimresb  15567  o1resb  15568  modfsummod  15798  isprm2  16683  isprm4  16685  isprm7  16709  acsfn2  17676  pgpfac1  20080  isirred2  20403  isdomn2OLD  20690  isdomn3  20693  islindf4  21836  coe1fzgsumd  22295  evl1gsumd  22348  ist1-2  23342  isnrm2  23353  dfconn2  23414  1stccn  23458  iskgen3  23544  hausdiag  23640  cnflf  23997  txflf  24001  cnfcf  24037  metcnp  24541  caucfil  25302  ovolgelb  25500  ismbl  25546  dyadmbllem  25619  itg2leub  25755  ellimc3  25899  mdegleb  26091  jensen  27017  dchrelbas2  27266  dchrelbas3  27267  eqscut2  27836  nmoubi  30705  nmobndseqi  30712  nmobndseqiALT  30713  h1dei  31483  nmopub  31841  nmfnleub  31858  mdsl1i  32254  mdsl2i  32255  elat2  32273  islinds5  33242  islbs5  33255  eulerpartlemgvv  34210  bnj115  34570  bnj1109  34631  bnj1533  34697  bnj580  34758  bnj864  34767  bnj865  34768  bnj1049  34819  bnj1090  34824  bnj1093  34825  bnj1133  34834  bnj1171  34845  climuzcnv  35499  axextprim  35523  biimpexp  35539  dfon2lem8  35614  dffun10  35738  filnetlem4  36093  bj-substax12  36426  wl-2sb6d  37253  poimirlem25  37346  poimirlem30  37351  ralin  37946  r2alan  37947  inxpss  38009  moantr  38062  isat3  39005  isltrn2N  39819  cdlemefrs29bpre0  40095  cdleme32fva  40136  sn-axrep5v  41938  dford4  42687  fnwe2lem2  42712  ifpidg  43158  ifpim23g  43162  elmapintrab  43243  undmrnresiss  43271  df3or2  43435  df3an2  43436  dfhe3  43442  dffrege76  43606  dffrege115  43645  ntrneiiso  43758  ismnushort  43975  pm11.62  44068  2sbc6g  44089  expcomdg  44176  impexpd  44189  dfvd2  44255  dfvd3  44267  rabssf  44720  2rexsb  46714  2rexrsb  46715  snlindsntor  47854  elbigo2  47940  exp12bd  48183  ralbidb  48187  ralbidc  48188

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »