Theorem expimpd 459

Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
expimpd.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
expimpd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 416	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ 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:  ornld  1077  3impia  1135  ralrimdva  3164  disjiun  5095  reusv3  5374  euotd  5494  swopo  5578  sotr3  5608  wereu2  5656  poirr2  6122  sossfld  6183  reuop  6295  frpomin  6342  ordpss  6390  oneqmini  6415  suctr  6450  elpreima  7054  fmptco  7126  isofrlem  7344  onmindif2  7809  resf1extb  7934  mptcnfimad  7986  frxp  8127  fnse  8134  suppss  8195  tposfo2  8250  wfr3g  8321  tz7.48-2  8434  omeulem1  8572  omeu  8575  nnaordex  8629  eldifsucnn  8655  pssnn  9166  onomeneq  9211  fodomfib  9301  dffi3  9404  supmo  9425  supnub  9435  infglb  9464  infnlb  9466  infmo  9470  infsupprpr  9479  cantnfle  9653  cantnflem1  9671  epfrs  9713  frr3g  9741  updjud  9942  alephord2i  10083  cardinfima  10103  aceq3lem  10126  dfac2b  10136  dfac12lem2  10150  axdc2lem  10453  ttukeylem6  10519  alephval2  10584  fpwwe2lem11  10653  fpwwe2lem12  10654  prlem934  11045  reclem4pr  11062  suplem1pr  11064  letr  11331  sup2  12198  uzind  12716  ledivge1le  13117  xrletr  13211  xltnegi  13270  xlemul1a  13342  ixxssixx  13414  difreicc  13539  flval3  13878  fsequb  14041  seqf1olem1  14107  expnegz  14162  hash2prd  14542  ccatrcl1  14663  relexprelg  15113  shftlem  15143  rexuzre  15442  cau3lem  15444  caubnd2  15447  caubnd  15448  climrlim2  15636  climuni  15641  2clim  15661  o1co  15675  rlimno1  15743  climbdd  15761  caurcvg  15766  summolem2  15804  summo  15805  zsum  15806  fsumf1o  15811  fsumss  15813  fsumcl2lem  15819  fsumadd  15828  fsummulc2  15872  fsumconst  15878  fsumrelem  15896  prodmolem2  16026  prodmo  16027  zprod  16028  fprodf1o  16037  fprodss  16039  fprodcl2lem  16041  fprodmul  16051  fproddiv  16052  fprodconst  16069  fprodn0  16070  dfgcd2  16640  lcmfunsnlem2  16734  coprmproddvdslem  16756  cncongrprm  16824  prmpwdvds  17000  infpnlem1  17006  1arith  17023  vdwapun  17070  vdwlem11  17087  vdwnnlem2  17092  ramz  17121  ramcl  17125  prmlem0  17201  firest  17521  catpropd  17801  initoid  18094  termoid  18095  initoeu2lem1  18107  pltnle  18428  pltletr  18433  pospo  18435  psss  18672  mgmn0plusgf  18745  isgrpid2  19104  f1omvdco2  19579  pgpfi  19736  frgpnabllem1  20004  gsumval3eu  20035  gsumzres  20040  gsumzcl2  20041  gsumzf1o  20043  gsumzaddlem  20052  gsumconst  20065  gsumzmhm  20068  gsumzoppg  20075  ablfaclem3  20220  dvdsrtr  20513  dvdsrmul1  20514  unitgrp  20528  domnmuln0  20875  lspsolvlem  21333  gsumfsum  21651  nzerooringczr  21697  obslbs  21947  gsummoncoe1  22537  pf1ind  22584  dmatscmcl  22729  scmatmulcl  22744  smatvscl  22750  mdetdiaglem  22824  matunitlindflem1  22905  cpmatinvcl  22946  mp2pm2mplem4  23038  cpmadugsumlemF  23105  eltg3  23191  tgidm  23209  neindisj  23346  tgrest  23388  restcld  23401  tgcn  23481  lmcnp  23533  iunconnlem  23656  2ndcredom  23679  2ndc1stc  23680  1stcrest  23682  2ndcrest  23683  2ndcdisj  23686  nllyrest  23716  nllyidm  23719  lfinpfin  23754  locfincmp  23756  ptpjpre1  23801  ptuni2  23806  ptbasin  23807  ptbasfi  23811  txbasval  23836  ptpjopn  23842  ptclsg  23845  dfac14lem  23847  xkoccn  23849  txcnp  23850  ptcnplem  23851  ptcnp  23852  txtube  23870  txcmplem1  23871  txcmplem2  23872  tx2ndc  23881  txkgen  23882  xkoco1cn  23887  xkoco2cn  23888  xkococnlem  23889  xkococn  23890  xkoinjcn  23917  qtoprest  23947  kqsat  23961  kqcldsat  23963  isfild  24088  fbunfip  24099  fgabs  24109  filconn  24113  fbasrn  24114  filufint  24150  elfm2  24178  elfm3  24180  fmfnfm  24188  hausflimi  24210  cnpflfi  24229  ptcmplem2  24283  tmdgsum2  24326  cldsubg  24341  qustgpopn  24350  ustfilxp  24443  bldisj  24628  xbln0  24644  blssps  24654  blss  24655  blssexps  24656  blssex  24657  blcls  24736  metcnp3  24770  icccmplem2  25054  mpomulcn  25099  cnheibor  25187  iscau4  25511  cmssmscld  25582  ovolshftlem2  25742  ovolicc2lem5  25753  dyadmax  25830  mbfi1fseqlem4  25950  mbfi1flimlem  25954  lhop1lem  26245  dvfsumrlim  26263  aalioulem3  26570  ulmcn  26635  radcnvlt1  26654  pilem2  26688  efopn  26896  cxpeq0  26916  cxpmul2z  26929  cxpcn3lem  26985  xrlimcnp  27206  vmappw  27353  fsumvma  27450  dchrptlem1  27501  lgsqr  27588  lgsdchrval  27591  2lgslem3  27641  2sqlem6  27660  2sqlem7  27661  2sqreultlem  27684  2sqreunnltlem  27687  pntlem3  27846  pntleml  27848  ltsval2  27893  nosupno  27940  nosupbnd1lem5  27949  noinfno  27955  lestr  27999  madebdayim  28154  ltslpss  28174  negsid  28307  noseqinds  28559  brbtwn  29357  brcgr  29358  axcontlem8  29429  nbumgrvtx  29807  cusgrfilem2  29917  1loopgrnb0  29963  uspgr2wlkeq  30106  wlklenvclwlk  30114  subgrwlk  30149  upgrwlkdvdelem  30202  uspgrn2crct  30277  0enwwlksnge1  30333  usgr2wspthons3  30436  clwwlkccatlem  30460  clwlkclwwlkf  30479  clwwlknonel  30566  frgrncvvdeqlem9  30788  frgr2wwlkeqm  30812  frgrreggt1  30874  frgrreg  30875  pjhthmo  31784  spansncvi  32134  nmcexi  32508  cnlnssadj  32562  leopmuli  32615  elpjrn  32672  mdsl0  32792  sumdmdii  32897  fmptcof2  33132  suppss3  33196  lmxrge0  34464  bnj594  35423  bnj849  35436  noinfepfnregs  35660  erdszelem7  35778  sconnpi1  35820  cvmsval  35847  cvmopnlem  35859  cvmfolem  35860  cvmliftmolem2  35863  cvmlift2lem10  35893  cvmlift2lem12  35895  cvmlift3lem5  35904  cvmlift3lem8  35907  satfv0  35939  satfv1  35944  satfvsucsuc  35946  satffunlem1lem2  35984  satffunlem2lem2  35987  linethru  36735  opnrebl2  36942  neibastop2lem  36981  neibastop2  36982  bj-cbv3ta  37531  cgsex2gd  37891  isinf2  38161  phpreu  38360  finixpnum  38361  lindsadd  38369  ptrecube  38371  poimirlem26  38397  poimirlem27  38398  poimirlem31  38402  poimir  38404  heicant  38406  voliunnfl  38415  volsupnfl  38416  itg2addnclem  38422  findcard4  38465  unirep  38466  sdclem2  38494  istotbnd3  38523  ssbnd  38540  eldisjlem19  39663  lshpdisj  39862  lsatn0  39874  lsat0cv  39908  cvrletrN  40148  cvrval4N  40289  lncvrelatN  40656  paddasslem14  40708  paddasslem15  40709  paddasslem16  40710  pmapjoin  40727  dihglblem2N  42169  dochvalr  42232  eqresfnbd  43104  sn-sup2  43381  prjspner1  43474  flt4lem7  43507  incssnn0  43558  eldioph4b  43654  diophren  43656  fphpdo  43660  rencldnfilem  43663  pellexlem5  43676  pell1234qrne0  43696  pell1234qrmulcl  43698  pell14qrgt0  43702  pell1234qrdich  43704  pell14qrdich  43712  pell1qrge1  43713  pell1qrgap  43717  pellfundre  43724  pellfundlb  43727  dvdsacongtr  43827  jm2.19lem4  43835  aomclem4  43900  hbtlem2  43967  hbtlem4  43969  hbtlem6  43972  cantnfresb  44167  dflim5  44172  tfsconcatrn  44185  tfsconcatrev  44191  naddwordnexlem4  44244  safesnsupfiss  44257  harval3  44380  clcnvlem  44465  relpfrlem  45778  cfsetsnfsetfo  47950  euoreqb  47999  2reu8i  48003  sprsymrelf1lem  48393  sprsymrelfolem2  48395  reupr  48424  fmtnofac2lem  48473  opoeALTV  48601  opeoALTV  48602  fpprwpprb  48658  gboge9  48682  clnbgrel  48746  grimco  48807  uhgrimedgi  48808  isuspgrim  48814  cycldlenngric  48846  uhgrimisgrgric  48849  clnbgrgrimlem  48851  clnbgrgrim  48852  grtriprop  48859  stgrusgra  48877  grlimedgclnbgr  48913  grlimprclnbgrvtx  48917  grlimgredgex  48918  grlictr  48933  gpgedg2iv  48985  gpgcubic  48997  gpg5nbgr3star  48999  pgnbgreunbgrlem2  49035  pgnbgreunbgrlem5  49041  ellcoellss  49367  nn0sumshdiglem1  49553  itschlc0xyqsol  49699  itsclc0  49703  opnneilv  49837