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  1115  ralrimdva  3112  disjiun  5057  reusv3  5323  euotd  5421  swopo  5505  wereu2  5577  poirr2  6018  sossfld  6078  reuop  6185  frpomin  6228  oneqmini  6302  suctr  6334  elpreima  6917  fmptco  6983  isofrlem  7191  onmindif2  7634  frxp  7938  fnse  7945  suppss  7981  suppssOLD  7982  tposfo2  8036  wfr3g  8109  tz7.48-2  8243  omeulem1  8375  omeu  8378  nnaordex  8431  pssnn  8913  pssnnOLD  8969  fodomfib  9023  dffi3  9120  supmo  9141  supnub  9151  infglb  9179  infnlb  9181  infmo  9184  infsupprpr  9193  cantnfle  9359  cantnflem1  9377  trpredrec  9415  epfrs  9420  frr3g  9445  updjud  9623  alephord2i  9764  cardinfima  9784  aceq3lem  9807  dfac2b  9817  dfac12lem2  9831  axdc2lem  10135  ttukeylem6  10201  alephval2  10259  fpwwe2lem11  10328  fpwwe2lem12  10329  prlem934  10720  reclem4pr  10737  suplem1pr  10739  letr  10999  sup2  11861  uzind  12342  ledivge1le  12730  xrletr  12821  xltnegi  12879  xlemul1a  12951  ixxssixx  13022  difreicc  13145  flval3  13463  fsequb  13623  seqf1olem1  13690  expnegz  13745  hash2prd  14117  ccatrcl1  14227  relexprelg  14677  shftlem  14707  rexuzre  14992  cau3lem  14994  caubnd2  14997  caubnd  14998  climrlim2  15184  climuni  15189  2clim  15209  o1co  15223  rlimno1  15293  climbdd  15311  caurcvg  15316  summolem2  15356  summo  15357  zsum  15358  fsumf1o  15363  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  fsummulc2  15424  fsumconst  15430  fsumrelem  15447  prodmolem2  15573  prodmo  15574  zprod  15575  fprodf1o  15584  fprodss  15586  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodconst  15616  fprodn0  15617  dfgcd2  16182  lcmfunsnlem2  16273  coprmproddvdslem  16295  cncongrprm  16361  prmpwdvds  16533  infpnlem1  16539  1arith  16556  vdwapun  16603  vdwlem11  16620  vdwnnlem2  16625  ramz  16654  ramcl  16658  prmlem0  16735  firest  17060  catpropd  17335  initoid  17632  termoid  17633  initoeu2lem1  17645  pltnle  17971  pltletr  17976  pospo  17978  psss  18213  isgrpid2  18531  f1omvdco2  18971  pgpfi  19125  frgpnabllem1  19389  gsumval3eu  19420  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  ablfaclem3  19605  dvdsrtr  19809  dvdsrmul1  19810  unitgrp  19824  lspsolvlem  20319  domnmuln0  20482  gsumfsum  20577  obslbs  20847  gsummoncoe1  21385  pf1ind  21431  dmatscmcl  21560  scmatmulcl  21575  smatvscl  21581  mdetdiaglem  21655  cpmatinvcl  21774  mp2pm2mplem4  21866  cpmadugsumlemF  21933  eltg3  22020  tgidm  22038  neindisj  22176  tgrest  22218  restcld  22231  tgcn  22311  lmcnp  22363  iunconnlem  22486  2ndcredom  22509  2ndc1stc  22510  1stcrest  22512  2ndcrest  22513  2ndcdisj  22515  nllyrest  22545  nllyidm  22548  lfinpfin  22583  locfincmp  22585  ptpjpre1  22630  ptuni2  22635  ptbasin  22636  ptbasfi  22640  txbasval  22665  ptpjopn  22671  ptclsg  22674  dfac14lem  22676  xkoccn  22678  txcnp  22679  ptcnplem  22680  ptcnp  22681  txtube  22699  txcmplem1  22700  txcmplem2  22701  tx2ndc  22710  txkgen  22711  xkoco1cn  22716  xkoco2cn  22717  xkococnlem  22718  xkococn  22719  xkoinjcn  22746  qtoprest  22776  kqsat  22790  kqcldsat  22792  isfild  22917  fbunfip  22928  fgabs  22938  filconn  22942  fbasrn  22943  filufint  22979  elfm2  23007  elfm3  23009  fmfnfm  23017  hausflimi  23039  cnpflfi  23058  ptcmplem2  23112  tmdgsum2  23155  cldsubg  23170  qustgpopn  23179  ustfilxp  23272  bldisj  23459  xbln0  23475  blssps  23485  blss  23486  blssexps  23487  blssex  23488  blcls  23568  metcnp3  23602  icccmplem2  23892  cnheibor  24024  iscau4  24348  cmssmscld  24419  ovolshftlem2  24579  ovolicc2lem5  24590  dyadmax  24667  mbfi1fseqlem4  24788  mbfi1flimlem  24792  lhop1lem  25082  dvfsumrlim  25100  aalioulem3  25399  ulmcn  25463  radcnvlt1  25482  pilem2  25516  efopn  25718  cxpeq0  25738  cxpmul2z  25751  cxpcn3lem  25805  xrlimcnp  26023  vmappw  26170  fsumvma  26266  dchrptlem1  26317  lgsqr  26404  lgsdchrval  26407  2lgslem3  26457  2sqlem6  26476  2sqlem7  26477  2sqreultlem  26500  2sqreunnltlem  26503  pntlem3  26662  pntleml  26664  brbtwn  27170  brcgr  27171  axcontlem8  27242  nbumgrvtx  27616  cusgrfilem2  27726  1loopgrnb0  27772  uspgr2wlkeq  27915  wlklenvclwlk  27924  upgrwlkdvdelem  28005  uspgrn2crct  28074  0enwwlksnge1  28130  usgr2wspthons3  28230  clwwlkccatlem  28254  clwlkclwwlkf  28273  clwwlknonel  28360  frgrncvvdeqlem9  28572  frgr2wwlkeqm  28596  frgrreggt1  28658  frgrreg  28659  pjhthmo  29565  spansncvi  29915  nmcexi  30289  cnlnssadj  30343  leopmuli  30396  elpjrn  30453  mdsl0  30573  sumdmdii  30678  fmptcof2  30896  suppss3  30961  lmxrge0  31804  bnj594  32792  bnj849  32805  subgrwlk  32994  erdszelem7  33059  sconnpi1  33101  cvmsval  33128  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem2  33144  cvmlift2lem10  33174  cvmlift2lem12  33176  cvmlift3lem5  33185  cvmlift3lem8  33188  satfv0  33220  satfv1  33225  satfvsucsuc  33227  satffunlem1lem2  33265  satffunlem2lem2  33268  eldifsucnn  33597  sotr3  33639  sltval2  33786  nosupno  33833  nosupbnd1lem5  33842  noinfno  33848  sletr  33888  madebdayim  33997  sltlpss  34014  linethru  34382  opnrebl2  34437  neibastop2lem  34476  neibastop2  34477  bj-cbv3ta  34895  isinf2  35503  phpreu  35688  finixpnum  35689  lindsadd  35697  matunitlindflem1  35700  ptrecube  35704  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimir  35737  heicant  35739  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  unirep  35798  sdclem2  35827  istotbnd3  35856  ssbnd  35873  lshpdisj  36928  lsatn0  36940  lsat0cv  36974  cvrletrN  37214  cvrval4N  37355  lncvrelatN  37722  paddasslem14  37774  paddasslem15  37775  paddasslem16  37776  pmapjoin  37793  dihglblem2N  39235  dochvalr  39298  sn-negex12  40319  sn-sup2  40360  prjspner1  40384  flt4lem7  40412  incssnn0  40449  eldioph4b  40549  diophren  40551  fphpdo  40555  rencldnfilem  40558  pellexlem5  40571  pell1234qrne0  40591  pell1234qrmulcl  40593  pell14qrgt0  40597  pell1234qrdich  40599  pell14qrdich  40607  pell1qrge1  40608  pell1qrgap  40612  pellfundre  40619  pellfundlb  40622  dvdsacongtr  40722  jm2.19lem4  40730  aomclem4  40798  hbtlem2  40865  hbtlem4  40867  hbtlem6  40870  harval3  41041  clcnvlem  41120  ordpss  41958  cfsetsnfsetfo  44441  euoreqb  44488  2reu8i  44492  sprsymrelf1lem  44831  sprsymrelfolem2  44833  reupr  44862  fmtnofac2lem  44908  opoeALTV  45023  opeoALTV  45024  fpprwpprb  45080  gboge9  45104  nzerooringczr  45518  ellcoellss  45664  nn0sumshdiglem1  45855  itschlc0xyqsol  46001  itsclc0  46005  opnneilv  46090