Theorem expimpd 453

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 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ 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 206  df-an 396

This theorem is referenced by:  ornld  1058  3impia  1114  ralrimdva  3146  disjiun  5126  reusv3  5394  euotd  5504  swopo  5590  sotr3  5618  wereu2  5664  poirr2  6116  sossfld  6176  reuop  6283  frpomin  6332  oneqmini  6407  suctr  6441  elpreima  7050  fmptco  7120  isofrlem  7330  onmindif2  7789  frxp  8107  fnse  8114  suppss  8174  suppssOLD  8175  tposfo2  8230  wfr3g  8303  tz7.48-2  8438  omeulem1  8578  omeu  8581  nnaordex  8634  eldifsucnn  8660  pssnn  9165  onomeneq  9225  pssnnOLD  9262  fodomfib  9323  dffi3  9423  supmo  9444  supnub  9454  infglb  9482  infnlb  9484  infmo  9487  infsupprpr  9496  cantnfle  9663  cantnflem1  9681  epfrs  9723  frr3g  9748  updjud  9926  alephord2i  10069  cardinfima  10089  aceq3lem  10112  dfac2b  10122  dfac12lem2  10136  axdc2lem  10440  ttukeylem6  10506  alephval2  10564  fpwwe2lem11  10633  fpwwe2lem12  10634  prlem934  11025  reclem4pr  11042  suplem1pr  11044  letr  11306  sup2  12168  uzind  12652  ledivge1le  13043  xrletr  13135  xltnegi  13193  xlemul1a  13265  ixxssixx  13336  difreicc  13459  flval3  13778  fsequb  13938  seqf1olem1  14005  expnegz  14060  hash2prd  14434  ccatrcl1  14542  relexprelg  14983  shftlem  15013  rexuzre  15297  cau3lem  15299  caubnd2  15302  caubnd  15303  climrlim2  15489  climuni  15494  2clim  15514  o1co  15528  rlimno1  15598  climbdd  15616  caurcvg  15621  summolem2  15660  summo  15661  zsum  15662  fsumf1o  15667  fsumss  15669  fsumcl2lem  15675  fsumadd  15684  fsummulc2  15728  fsumconst  15734  fsumrelem  15751  prodmolem2  15877  prodmo  15878  zprod  15879  fprodf1o  15888  fprodss  15890  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodconst  15920  fprodn0  15921  dfgcd2  16487  lcmfunsnlem2  16576  coprmproddvdslem  16598  cncongrprm  16666  prmpwdvds  16838  infpnlem1  16844  1arith  16861  vdwapun  16908  vdwlem11  16925  vdwnnlem2  16930  ramz  16959  ramcl  16963  prmlem0  17040  firest  17379  catpropd  17654  initoid  17955  termoid  17956  initoeu2lem1  17968  pltnle  18295  pltletr  18300  pospo  18302  psss  18537  isgrpid2  18898  f1omvdco2  19360  pgpfi  19517  frgpnabllem1  19785  gsumval3eu  19816  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  ablfaclem3  20001  dvdsrtr  20262  dvdsrmul1  20263  unitgrp  20277  lspsolvlem  20985  domnmuln0  21200  gsumfsum  21298  nzerooringczr  21337  obslbs  21595  gsummoncoe1  22151  pf1ind  22198  dmatscmcl  22329  scmatmulcl  22344  smatvscl  22350  mdetdiaglem  22424  cpmatinvcl  22543  mp2pm2mplem4  22635  cpmadugsumlemF  22702  eltg3  22789  tgidm  22807  neindisj  22945  tgrest  22987  restcld  23000  tgcn  23080  lmcnp  23132  iunconnlem  23255  2ndcredom  23278  2ndc1stc  23279  1stcrest  23281  2ndcrest  23282  2ndcdisj  23284  nllyrest  23314  nllyidm  23317  lfinpfin  23352  locfincmp  23354  ptpjpre1  23399  ptuni2  23404  ptbasin  23405  ptbasfi  23409  txbasval  23434  ptpjopn  23440  ptclsg  23443  dfac14lem  23445  xkoccn  23447  txcnp  23448  ptcnplem  23449  ptcnp  23450  txtube  23468  txcmplem1  23469  txcmplem2  23470  tx2ndc  23479  txkgen  23480  xkoco1cn  23485  xkoco2cn  23486  xkococnlem  23487  xkococn  23488  xkoinjcn  23515  qtoprest  23545  kqsat  23559  kqcldsat  23561  isfild  23686  fbunfip  23697  fgabs  23707  filconn  23711  fbasrn  23712  filufint  23748  elfm2  23776  elfm3  23778  fmfnfm  23786  hausflimi  23808  cnpflfi  23827  ptcmplem2  23881  tmdgsum2  23924  cldsubg  23939  qustgpopn  23948  ustfilxp  24041  bldisj  24228  xbln0  24244  blssps  24254  blss  24255  blssexps  24256  blssex  24257  blcls  24339  metcnp3  24373  icccmplem2  24663  mpomulcn  24709  cnheibor  24805  iscau4  25131  cmssmscld  25202  ovolshftlem2  25363  ovolicc2lem5  25374  dyadmax  25451  mbfi1fseqlem4  25572  mbfi1flimlem  25576  lhop1lem  25870  dvfsumrlim  25890  aalioulem3  26190  ulmcn  26254  radcnvlt1  26273  pilem2  26308  efopn  26511  cxpeq0  26531  cxpmul2z  26544  cxpcn3lem  26601  xrlimcnp  26819  vmappw  26967  fsumvma  27065  dchrptlem1  27116  lgsqr  27203  lgsdchrval  27206  2lgslem3  27256  2sqlem6  27275  2sqlem7  27276  2sqreultlem  27299  2sqreunnltlem  27302  pntlem3  27461  pntleml  27463  sltval2  27508  nosupno  27555  nosupbnd1lem5  27564  noinfno  27570  sletr  27610  madebdayim  27733  sltlpss  27752  negsid  27872  noseqinds  28085  brbtwn  28629  brcgr  28630  axcontlem8  28701  nbumgrvtx  29075  cusgrfilem2  29185  1loopgrnb0  29231  uspgr2wlkeq  29375  wlklenvclwlk  29384  upgrwlkdvdelem  29465  uspgrn2crct  29534  0enwwlksnge1  29590  usgr2wspthons3  29690  clwwlkccatlem  29714  clwlkclwwlkf  29733  clwwlknonel  29820  frgrncvvdeqlem9  30032  frgr2wwlkeqm  30056  frgrreggt1  30118  frgrreg  30119  pjhthmo  31027  spansncvi  31377  nmcexi  31751  cnlnssadj  31805  leopmuli  31858  elpjrn  31915  mdsl0  32035  sumdmdii  32140  fmptcof2  32354  suppss3  32421  lmxrge0  33424  bnj594  34414  bnj849  34427  subgrwlk  34614  erdszelem7  34679  sconnpi1  34721  cvmsval  34748  cvmopnlem  34760  cvmfolem  34761  cvmliftmolem2  34764  cvmlift2lem10  34794  cvmlift2lem12  34796  cvmlift3lem5  34805  cvmlift3lem8  34808  satfv0  34840  satfv1  34845  satfvsucsuc  34847  satffunlem1lem2  34885  satffunlem2lem2  34888  linethru  35621  opnrebl2  35697  neibastop2lem  35736  neibastop2  35737  bj-cbv3ta  36155  isinf2  36777  phpreu  36966  finixpnum  36967  lindsadd  36975  matunitlindflem1  36978  ptrecube  36982  poimirlem26  37008  poimirlem27  37009  poimirlem31  37013  poimir  37015  heicant  37017  voliunnfl  37026  volsupnfl  37027  itg2addnclem  37033  unirep  37076  sdclem2  37104  istotbnd3  37133  ssbnd  37150  eldisjlem19  38174  lshpdisj  38351  lsatn0  38363  lsat0cv  38397  cvrletrN  38637  cvrval4N  38779  lncvrelatN  39146  paddasslem14  39198  paddasslem15  39199  paddasslem16  39200  pmapjoin  39217  dihglblem2N  40659  dochvalr  40722  eqresfnbd  41551  sn-negex12  41803  sn-sup2  41856  prjspner1  41882  flt4lem7  41915  incssnn0  41963  eldioph4b  42063  diophren  42065  fphpdo  42069  rencldnfilem  42072  pellexlem5  42085  pell1234qrne0  42105  pell1234qrmulcl  42107  pell14qrgt0  42111  pell1234qrdich  42113  pell14qrdich  42121  pell1qrge1  42122  pell1qrgap  42126  pellfundre  42133  pellfundlb  42136  dvdsacongtr  42237  jm2.19lem4  42245  aomclem4  42313  hbtlem2  42380  hbtlem4  42382  hbtlem6  42385  cantnfresb  42588  dflim5  42593  tfsconcatrn  42606  tfsconcatrev  42612  naddwordnexlem4  42666  safesnsupfiss  42680  harval3  42803  clcnvlem  42888  ordpss  43724  cfsetsnfsetfo  46280  euoreqb  46327  2reu8i  46331  sprsymrelf1lem  46669  sprsymrelfolem2  46671  reupr  46700  fmtnofac2lem  46746  opoeALTV  46861  opeoALTV  46862  fpprwpprb  46918  gboge9  46942  ellcoellss  47329  nn0sumshdiglem1  47520  itschlc0xyqsol  47666  itsclc0  47670  opnneilv  47753