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 207  df-an 396

This theorem is referenced by:  ornld  1061  3impia  1117  ralrimdva  3133  disjiun  5095  reusv3  5360  euotd  5473  swopo  5557  sotr3  5587  wereu2  5635  poirr2  6097  sossfld  6159  reuop  6266  frpomin  6313  oneqmini  6385  suctr  6420  elpreima  7030  fmptco  7101  isofrlem  7315  onmindif2  7783  resf1extb  7910  mptcnfimad  7965  frxp  8105  fnse  8112  suppss  8173  tposfo2  8228  wfr3g  8298  tz7.48-2  8410  omeulem1  8546  omeu  8549  nnaordex  8602  eldifsucnn  8628  pssnn  9132  onomeneq  9178  fodomfib  9280  fodomfibOLD  9282  dffi3  9382  supmo  9403  supnub  9413  infglb  9442  infnlb  9444  infmo  9448  infsupprpr  9457  cantnfle  9624  cantnflem1  9642  epfrs  9684  frr3g  9709  updjud  9887  alephord2i  10030  cardinfima  10050  aceq3lem  10073  dfac2b  10084  dfac12lem2  10098  axdc2lem  10401  ttukeylem6  10467  alephval2  10525  fpwwe2lem11  10594  fpwwe2lem12  10595  prlem934  10986  reclem4pr  11003  suplem1pr  11005  letr  11268  sup2  12139  uzind  12626  ledivge1le  13024  xrletr  13118  xltnegi  13176  xlemul1a  13248  ixxssixx  13320  difreicc  13445  flval3  13777  fsequb  13940  seqf1olem1  14006  expnegz  14061  hash2prd  14440  ccatrcl1  14559  relexprelg  15004  shftlem  15034  rexuzre  15319  cau3lem  15321  caubnd2  15324  caubnd  15325  climrlim2  15513  climuni  15518  2clim  15538  o1co  15552  rlimno1  15620  climbdd  15638  caurcvg  15643  summolem2  15682  summo  15683  zsum  15684  fsumf1o  15689  fsumss  15691  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumconst  15756  fsumrelem  15773  prodmolem2  15901  prodmo  15902  zprod  15903  fprodf1o  15912  fprodss  15914  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodconst  15944  fprodn0  15945  dfgcd2  16516  lcmfunsnlem2  16610  coprmproddvdslem  16632  cncongrprm  16699  prmpwdvds  16875  infpnlem1  16881  1arith  16898  vdwapun  16945  vdwlem11  16962  vdwnnlem2  16967  ramz  16996  ramcl  17000  prmlem0  17076  firest  17395  catpropd  17670  initoid  17963  termoid  17964  initoeu2lem1  17976  pltnle  18297  pltletr  18302  pospo  18304  psss  18539  isgrpid2  18908  f1omvdco2  19378  pgpfi  19535  frgpnabllem1  19803  gsumval3eu  19834  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  ablfaclem3  20019  dvdsrtr  20277  dvdsrmul1  20278  unitgrp  20292  domnmuln0  20618  lspsolvlem  21052  gsumfsum  21351  nzerooringczr  21390  obslbs  21639  gsummoncoe1  22195  pf1ind  22242  dmatscmcl  22390  scmatmulcl  22405  smatvscl  22411  mdetdiaglem  22485  cpmatinvcl  22604  mp2pm2mplem4  22696  cpmadugsumlemF  22763  eltg3  22849  tgidm  22867  neindisj  23004  tgrest  23046  restcld  23059  tgcn  23139  lmcnp  23191  iunconnlem  23314  2ndcredom  23337  2ndc1stc  23338  1stcrest  23340  2ndcrest  23341  2ndcdisj  23343  nllyrest  23373  nllyidm  23376  lfinpfin  23411  locfincmp  23413  ptpjpre1  23458  ptuni2  23463  ptbasin  23464  ptbasfi  23468  txbasval  23493  ptpjopn  23499  ptclsg  23502  dfac14lem  23504  xkoccn  23506  txcnp  23507  ptcnplem  23508  ptcnp  23509  txtube  23527  txcmplem1  23528  txcmplem2  23529  tx2ndc  23538  txkgen  23539  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  qtoprest  23604  kqsat  23618  kqcldsat  23620  isfild  23745  fbunfip  23756  fgabs  23766  filconn  23770  fbasrn  23771  filufint  23807  elfm2  23835  elfm3  23837  fmfnfm  23845  hausflimi  23867  cnpflfi  23886  ptcmplem2  23940  tmdgsum2  23983  cldsubg  23998  qustgpopn  24007  ustfilxp  24100  bldisj  24286  xbln0  24302  blssps  24312  blss  24313  blssexps  24314  blssex  24315  blcls  24394  metcnp3  24428  icccmplem2  24712  mpomulcn  24758  cnheibor  24854  iscau4  25179  cmssmscld  25250  ovolshftlem2  25411  ovolicc2lem5  25422  dyadmax  25499  mbfi1fseqlem4  25619  mbfi1flimlem  25623  lhop1lem  25918  dvfsumrlim  25938  aalioulem3  26242  ulmcn  26308  radcnvlt1  26327  pilem2  26362  efopn  26567  cxpeq0  26587  cxpmul2z  26600  cxpcn3lem  26657  xrlimcnp  26878  vmappw  27026  fsumvma  27124  dchrptlem1  27175  lgsqr  27262  lgsdchrval  27265  2lgslem3  27315  2sqlem6  27334  2sqlem7  27335  2sqreultlem  27358  2sqreunnltlem  27361  pntlem3  27520  pntleml  27522  sltval2  27568  nosupno  27615  nosupbnd1lem5  27624  noinfno  27630  sletr  27670  madebdayim  27799  sltlpss  27819  negsid  27947  noseqinds  28187  brbtwn  28826  brcgr  28827  axcontlem8  28898  nbumgrvtx  29273  cusgrfilem2  29384  1loopgrnb0  29430  uspgr2wlkeq  29574  wlklenvclwlk  29583  upgrwlkdvdelem  29666  uspgrn2crct  29738  0enwwlksnge1  29794  usgr2wspthons3  29894  clwwlkccatlem  29918  clwlkclwwlkf  29937  clwwlknonel  30024  frgrncvvdeqlem9  30236  frgr2wwlkeqm  30260  frgrreggt1  30322  frgrreg  30323  pjhthmo  31231  spansncvi  31581  nmcexi  31955  cnlnssadj  32009  leopmuli  32062  elpjrn  32119  mdsl0  32239  sumdmdii  32344  fmptcof2  32581  suppss3  32647  lmxrge0  33942  bnj594  34902  bnj849  34915  subgrwlk  35119  erdszelem7  35184  sconnpi1  35226  cvmsval  35253  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem2  35269  cvmlift2lem10  35299  cvmlift2lem12  35301  cvmlift3lem5  35310  cvmlift3lem8  35313  satfv0  35345  satfv1  35350  satfvsucsuc  35352  satffunlem1lem2  35390  satffunlem2lem2  35393  linethru  36141  opnrebl2  36309  neibastop2lem  36348  neibastop2  36349  bj-cbv3ta  36774  isinf2  37393  phpreu  37598  finixpnum  37599  lindsadd  37607  matunitlindflem1  37610  ptrecube  37614  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimir  37647  heicant  37649  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  unirep  37708  sdclem2  37736  istotbnd3  37765  ssbnd  37782  eldisjlem19  38802  lshpdisj  38980  lsatn0  38992  lsat0cv  39026  cvrletrN  39266  cvrval4N  39408  lncvrelatN  39775  paddasslem14  39827  paddasslem15  39828  paddasslem16  39829  pmapjoin  39846  dihglblem2N  41288  dochvalr  41351  eqresfnbd  42220  sn-sup2  42479  prjspner1  42614  flt4lem7  42647  incssnn0  42699  eldioph4b  42799  diophren  42801  fphpdo  42805  rencldnfilem  42808  pellexlem5  42821  pell1234qrne0  42841  pell1234qrmulcl  42843  pell14qrgt0  42847  pell1234qrdich  42849  pell14qrdich  42857  pell1qrge1  42858  pell1qrgap  42862  pellfundre  42869  pellfundlb  42872  dvdsacongtr  42973  jm2.19lem4  42981  aomclem4  43046  hbtlem2  43113  hbtlem4  43115  hbtlem6  43118  cantnfresb  43313  dflim5  43318  tfsconcatrn  43331  tfsconcatrev  43337  naddwordnexlem4  43390  safesnsupfiss  43404  harval3  43527  clcnvlem  43612  ordpss  44440  relpfrlem  44943  cfsetsnfsetfo  47061  euoreqb  47110  2reu8i  47114  sprsymrelf1lem  47492  sprsymrelfolem2  47494  reupr  47523  fmtnofac2lem  47569  opoeALTV  47684  opeoALTV  47685  fpprwpprb  47741  gboge9  47765  clnbgrel  47829  grimco  47889  uhgrimedgi  47890  isuspgrim  47896  cycldlenngric  47928  uhgrimisgrgric  47931  clnbgrgrimlem  47933  clnbgrgrim  47934  grtriprop  47940  stgrusgra  47958  grlictr  48007  gpgedg2iv  48058  gpgcubic  48070  gpg5nbgr3star  48072  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem5  48113  ellcoellss  48424  nn0sumshdiglem1  48610  itschlc0xyqsol  48756  itsclc0  48760  opnneilv  48897