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  3166  disjiun  5094  reusv3  5371  euotd  5490  swopo  5574  sotr3  5604  wereu2  5652  poirr2  6130  sossfld  6190  reuop  6314  frpomin  6361  ordpss  6409  oneqmini  6434  suctr  6469  elpreimaOLD  7081  fmptco  7154  isofrlem  7371  onmindif2  7845  resf1extb  7970  mptcnfimad  8022  frxp  8165  fnse  8177  suppss  8239  tposfo2  8294  wfr3g  8365  tz7.48-2  8480  omeulem1  8618  omeu  8621  nnaordex  8675  eldifsucnn  8701  pssnn  9212  onomeneq  9257  fodomfib  9348  dffi3  9450  supmo  9471  supnub  9481  infglb  9510  infnlb  9512  infmo  9516  infsupprpr  9525  cantnfle  9699  cantnflem1  9717  epfrs  9759  frr3g  9787  updjud  10042  alephord2i  10183  cardinfima  10203  aceq3lem  10226  dfac2b  10236  dfac12lem2  10250  axdc2lem  10553  ttukeylem6  10619  alephval2  10684  fpwwe2lem11  10753  fpwwe2lem12  10754  prlem934  11145  reclem4pr  11162  suplem1pr  11164  letr  11431  sup2  12300  uzind  12818  ledivge1le  13220  xrletr  13314  xltnegi  13373  xlemul1a  13445  ixxssixx  13517  difreicc  13642  flval3  13982  fsequb  14145  seqf1olem1  14211  expnegz  14266  hash2prd  14647  ccatrcl1  14768  relexprelg  15220  shftlem  15250  rexuzre  15549  cau3lem  15551  caubnd2  15554  caubnd  15555  climrlim2  15743  climuni  15748  2clim  15768  o1co  15782  rlimno1  15850  climbdd  15868  caurcvg  15873  summolem2  15911  summo  15912  zsum  15913  fsumf1o  15918  fsumss  15920  fsumcl2lem  15926  fsumadd  15935  fsummulc2  15979  fsumconst  15985  fsumrelem  16003  prodmolem2  16131  prodmo  16132  zprod  16133  fprodf1o  16142  fprodss  16144  fprodcl2lem  16146  fprodmul  16156  fproddiv  16157  fprodconst  16174  fprodn0  16175  dfgcd2  16748  lcmfunsnlem2  16844  coprmproddvdslem  16866  cncongrprm  16934  prmpwdvds  17111  infpnlem1  17117  1arith  17134  vdwapun  17181  vdwlem11  17198  vdwnnlem2  17203  ramz  17232  ramcl  17236  prmlem0  17312  firest  17632  catpropd  17912  initoid  18205  termoid  18206  initoeu2lem1  18218  pltnle  18539  pltletr  18544  pospo  18546  psss  18783  mgmn0plusgf  18856  isgrpid2  19216  f1omvdco2  19692  pgpfi  19849  frgpnabllem1  20117  gsumval3eu  20148  gsumzres  20153  gsumzcl2  20154  gsumzf1o  20156  gsumzaddlem  20165  gsumconst  20178  gsumzmhm  20181  gsumzoppg  20188  ablfaclem3  20333  dvdsrtr  20628  dvdsrmul1  20629  unitgrp  20643  domnmuln0  20991  lspsolvlem  21450  gsumfsum  21770  nzerooringczr  21816  obslbs  22066  gsummoncoe1  22656  pf1ind  22703  dmatscmcl  22848  scmatmulcl  22863  smatvscl  22869  mdetdiaglem  22943  matunitlindflem1  23024  cpmatinvcl  23065  mp2pm2mplem4  23157  cpmadugsumlemF  23224  eltg3  23310  tgidm  23328  neindisj  23465  tgrest  23507  restcld  23520  tgcn  23600  lmcnp  23652  iunconnlem  23775  2ndcredom  23798  2ndc1stc  23799  1stcrest  23801  2ndcrest  23802  2ndcdisj  23805  nllyrest  23835  nllyidm  23838  lfinpfin  23873  locfincmp  23875  ptpjpre1  23920  ptuni2  23925  ptbasin  23926  ptbasfi  23930  txbasval  23955  ptpjopn  23961  ptclsg  23964  dfac14lem  23966  xkoccn  23968  txcnp  23969  ptcnplem  23970  ptcnp  23971  txtube  23989  txcmplem1  23990  txcmplem2  23991  tx2ndc  24000  txkgen  24001  xkoco1cn  24006  xkoco2cn  24007  xkococnlem  24008  xkococn  24009  xkoinjcn  24036  qtoprest  24066  kqsat  24080  kqcldsat  24082  isfild  24207  fbunfip  24218  fgabs  24228  filconn  24232  fbasrn  24233  filufint  24269  elfm2  24297  elfm3  24299  fmfnfm  24307  hausflimi  24329  cnpflfi  24348  ptcmplem2  24402  tmdgsum2  24445  cldsubg  24460  qustgpopn  24469  ustfilxp  24562  bldisj  24747  xbln0  24763  blssps  24773  blss  24774  blssexps  24775  blssex  24776  blcls  24855  metcnp3  24889  icccmplem2  25173  mpomulcn  25218  cnheibor  25306  iscau4  25630  cmssmscld  25701  ovolshftlem2  25861  ovolicc2lem5  25872  dyadmax  25949  mbfi1fseqlem4  26069  mbfi1flimlem  26073  lhop1lem  26363  dvfsumrlim  26381  aalioulem3  26691  ulmcn  26756  radcnvlt1  26775  pilem2  26809  efopn  27016  cxpeq0  27036  cxpmul2z  27049  cxpcn3lem  27105  xrlimcnp  27326  vmappw  27473  fsumvma  27570  dchrptlem1  27621  lgsqr  27708  lgsdchrval  27711  2lgslem3  27761  2sqlem6  27780  2sqlem7  27781  2sqreultlem  27804  2sqreunnltlem  27807  pntlem3  27966  pntleml  27968  flt4lem7  28019  ltsval2  28043  nosupno  28090  nosupbnd1lem5  28099  noinfno  28105  lestr  28149  madebdayim  28304  ltslpss  28324  negsid  28457  noseqinds  28709  brbtwn  29507  brcgr  29508  axcontlem8  29579  nbumgrvtx  29957  cusgrfilem2  30067  1loopgrnb0  30113  uspgr2wlkeq  30256  wlklenvclwlk  30264  subgrwlk  30299  upgrwlkdvdelem  30352  uspgrn2crct  30427  0enwwlksnge1  30483  usgr2wspthons3  30586  clwwlkccatlem  30610  clwlkclwwlkf  30629  clwwlknonel  30716  frgrncvvdeqlem9  30938  frgr2wwlkeqm  30962  frgrreggt1  31024  frgrreg  31025  pjhthmo  31934  spansncvi  32284  nmcexi  32658  cnlnssadj  32712  leopmuli  32765  elpjrn  32822  mdsl0  32942  sumdmdii  33047  fmptcof2  33323  suppss3  33385  lmxrge0  34654  bnj594  35612  bnj849  35625  noinfepfnregs  35900  erdszelem7  36129  sconnpi1  36171  cvmsval  36198  cvmopnlem  36210  cvmfolem  36211  cvmliftmolem2  36214  cvmlift2lem10  36244  cvmlift2lem12  36246  cvmlift3lem5  36255  cvmlift3lem8  36258  satfv0  36290  satfv1  36295  satfvsucsuc  36297  satffunlem1lem2  36335  satffunlem2lem2  36338  linethru  37096  opnrebl2  37287  neibastop2lem  37326  neibastop2  37327  bj-cbv3ta  37876  cgsex2gd  38250  isinf2  38520  phpreu  38719  finixpnum  38720  lindsadd  38728  ptrecube  38730  poimirlem26  38756  poimirlem27  38757  poimirlem31  38761  poimir  38763  heicant  38765  voliunnfl  38774  volsupnfl  38775  itg2addnclem  38781  findcard4  38824  unirep  38840  sdclem2  38868  istotbnd3  38897  ssbnd  38914  eldisjlem19  40037  lshpdisj  40236  lsatn0  40248  lsat0cv  40282  cvrletrN  40522  cvrval4N  40663  lncvrelatN  41030  paddasslem14  41082  paddasslem15  41083  paddasslem16  41084  pmapjoin  41101  dihglblem2N  42543  dochvalr  42606  eqresfnbd  43479  sn-sup2  43748  incssnn0  43915  eldioph4b  44011  diophren  44013  fphpdo  44017  rencldnfilem  44020  pellexlem5  44033  pell1234qrne0  44053  pell1234qrmulcl  44055  pell14qrgt0  44059  pell1234qrdich  44061  pell14qrdich  44069  pell1qrge1  44070  pell1qrgap  44074  pellfundre  44081  pellfundlb  44084  dvdsacongtr  44184  jm2.19lem4  44192  aomclem4  44252  hbtlem2  44318  hbtlem4  44320  hbtlem6  44323  cantnfresb  44518  dflim5  44523  tfsconcatrn  44536  tfsconcatrev  44542  naddwordnexlem4  44595  safesnsupfiss  44608  harval3  44731  clcnvlem  44815  relpfrlem  46138  cfsetsnfsetfo  48335  euoreqb  48385  2reu8i  48389  sprsymrelf1lem  48778  sprsymrelfolem2  48780  reupr  48809  fmtnofac2lem  48858  opoeALTV  48986  opeoALTV  48987  fpprwpprb  49043  gboge9  49067  clnbgrel  49131  grimco  49192  uhgrimedgi  49193  isuspgrim  49199  cycldlenngric  49231  uhgrimisgrgric  49234  clnbgrgrimlem  49236  clnbgrgrim  49237  grtriprop  49244  stgrusgra  49262  grlimedgclnbgr  49298  grlimprclnbgrvtx  49302  grlimgredgex  49303  grlictr  49318  gpgedg2iv  49370  gpgcubic  49382  gpg5nbgr3star  49384  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem5  49426  ellcoellss  49752  nn0sumshdiglem1  49938  itschlc0xyqsol  50084  itsclc0  50088  opnneilv  50228