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  3162  disjiun  5090  reusv3  5366  euotd  5482  swopo  5566  sotr3  5596  wereu2  5644  poirr2  6112  sossfld  6173  reuop  6285  frpomin  6332  ordpss  6380  oneqmini  6405  suctr  6440  elpreima  7045  fmptco  7118  isofrlem  7336  onmindif2  7804  resf1extb  7929  mptcnfimad  7981  frxp  8121  fnse  8128  suppss  8189  tposfo2  8244  wfr3g  8315  tz7.48-2  8430  omeulem1  8568  omeu  8571  nnaordex  8625  eldifsucnn  8651  pssnn  9162  onomeneq  9207  fodomfib  9298  dffi3  9401  supmo  9422  supnub  9432  infglb  9461  infnlb  9463  infmo  9467  infsupprpr  9476  cantnfle  9650  cantnflem1  9668  epfrs  9710  frr3g  9738  updjud  9987  alephord2i  10128  cardinfima  10148  aceq3lem  10171  dfac2b  10181  dfac12lem2  10195  axdc2lem  10498  ttukeylem6  10564  alephval2  10629  fpwwe2lem11  10698  fpwwe2lem12  10699  prlem934  11090  reclem4pr  11107  suplem1pr  11109  letr  11376  sup2  12243  uzind  12761  ledivge1le  13163  xrletr  13257  xltnegi  13316  xlemul1a  13388  ixxssixx  13460  difreicc  13585  flval3  13924  fsequb  14087  seqf1olem1  14153  expnegz  14208  hash2prd  14588  ccatrcl1  14709  relexprelg  15159  shftlem  15189  rexuzre  15488  cau3lem  15490  caubnd2  15493  caubnd  15494  climrlim2  15682  climuni  15687  2clim  15707  o1co  15721  rlimno1  15789  climbdd  15807  caurcvg  15812  summolem2  15850  summo  15851  zsum  15852  fsumf1o  15857  fsumss  15859  fsumcl2lem  15865  fsumadd  15874  fsummulc2  15918  fsumconst  15924  fsumrelem  15942  prodmolem2  16070  prodmo  16071  zprod  16072  fprodf1o  16081  fprodss  16083  fprodcl2lem  16085  fprodmul  16095  fproddiv  16096  fprodconst  16113  fprodn0  16114  dfgcd2  16684  lcmfunsnlem2  16778  coprmproddvdslem  16800  cncongrprm  16868  prmpwdvds  17044  infpnlem1  17050  1arith  17067  vdwapun  17114  vdwlem11  17131  vdwnnlem2  17136  ramz  17165  ramcl  17169  prmlem0  17245  firest  17565  catpropd  17845  initoid  18138  termoid  18139  initoeu2lem1  18151  pltnle  18472  pltletr  18477  pospo  18479  psss  18716  mgmn0plusgf  18789  isgrpid2  19149  f1omvdco2  19624  pgpfi  19781  frgpnabllem1  20049  gsumval3eu  20080  gsumzres  20085  gsumzcl2  20086  gsumzf1o  20088  gsumzaddlem  20097  gsumconst  20110  gsumzmhm  20113  gsumzoppg  20120  ablfaclem3  20265  dvdsrtr  20560  dvdsrmul1  20561  unitgrp  20575  domnmuln0  20923  lspsolvlem  21382  gsumfsum  21702  nzerooringczr  21748  obslbs  21998  gsummoncoe1  22588  pf1ind  22635  dmatscmcl  22780  scmatmulcl  22795  smatvscl  22801  mdetdiaglem  22875  matunitlindflem1  22956  cpmatinvcl  22997  mp2pm2mplem4  23089  cpmadugsumlemF  23156  eltg3  23242  tgidm  23260  neindisj  23397  tgrest  23439  restcld  23452  tgcn  23532  lmcnp  23584  iunconnlem  23707  2ndcredom  23730  2ndc1stc  23731  1stcrest  23733  2ndcrest  23734  2ndcdisj  23737  nllyrest  23767  nllyidm  23770  lfinpfin  23805  locfincmp  23807  ptpjpre1  23852  ptuni2  23857  ptbasin  23858  ptbasfi  23862  txbasval  23887  ptpjopn  23893  ptclsg  23896  dfac14lem  23898  xkoccn  23900  txcnp  23901  ptcnplem  23902  ptcnp  23903  txtube  23921  txcmplem1  23922  txcmplem2  23923  tx2ndc  23932  txkgen  23933  xkoco1cn  23938  xkoco2cn  23939  xkococnlem  23940  xkococn  23941  xkoinjcn  23968  qtoprest  23998  kqsat  24012  kqcldsat  24014  isfild  24139  fbunfip  24150  fgabs  24160  filconn  24164  fbasrn  24165  filufint  24201  elfm2  24229  elfm3  24231  fmfnfm  24239  hausflimi  24261  cnpflfi  24280  ptcmplem2  24334  tmdgsum2  24377  cldsubg  24392  qustgpopn  24401  ustfilxp  24494  bldisj  24679  xbln0  24695  blssps  24705  blss  24706  blssexps  24707  blssex  24708  blcls  24787  metcnp3  24821  icccmplem2  25105  mpomulcn  25150  cnheibor  25238  iscau4  25562  cmssmscld  25633  ovolshftlem2  25793  ovolicc2lem5  25804  dyadmax  25881  mbfi1fseqlem4  26001  mbfi1flimlem  26005  lhop1lem  26295  dvfsumrlim  26313  aalioulem3  26625  ulmcn  26690  radcnvlt1  26709  pilem2  26743  efopn  26950  cxpeq0  26970  cxpmul2z  26983  cxpcn3lem  27039  xrlimcnp  27260  vmappw  27407  fsumvma  27504  dchrptlem1  27555  lgsqr  27642  lgsdchrval  27645  2lgslem3  27695  2sqlem6  27714  2sqlem7  27715  2sqreultlem  27738  2sqreunnltlem  27741  pntlem3  27900  pntleml  27902  ltsval2  27947  nosupno  27994  nosupbnd1lem5  28003  noinfno  28009  lestr  28053  madebdayim  28208  ltslpss  28228  negsid  28361  noseqinds  28613  brbtwn  29411  brcgr  29412  axcontlem8  29483  nbumgrvtx  29861  cusgrfilem2  29971  1loopgrnb0  30017  uspgr2wlkeq  30160  wlklenvclwlk  30168  subgrwlk  30203  upgrwlkdvdelem  30256  uspgrn2crct  30331  0enwwlksnge1  30387  usgr2wspthons3  30490  clwwlkccatlem  30514  clwlkclwwlkf  30533  clwwlknonel  30620  frgrncvvdeqlem9  30842  frgr2wwlkeqm  30866  frgrreggt1  30928  frgrreg  30929  pjhthmo  31838  spansncvi  32188  nmcexi  32562  cnlnssadj  32616  leopmuli  32669  elpjrn  32726  mdsl0  32846  sumdmdii  32951  fmptcof2  33185  suppss3  33249  lmxrge0  34518  bnj594  35477  bnj849  35490  noinfepfnregs  35725  erdszelem7  35883  sconnpi1  35925  cvmsval  35952  cvmopnlem  35964  cvmfolem  35965  cvmliftmolem2  35968  cvmlift2lem10  35998  cvmlift2lem12  36000  cvmlift3lem5  36009  cvmlift3lem8  36012  satfv0  36044  satfv1  36049  satfvsucsuc  36051  satffunlem1lem2  36089  satffunlem2lem2  36092  linethru  36840  opnrebl2  37031  neibastop2lem  37070  neibastop2  37071  bj-cbv3ta  37620  cgsex2gd  37978  isinf2  38248  phpreu  38447  finixpnum  38448  lindsadd  38456  ptrecube  38458  poimirlem26  38484  poimirlem27  38485  poimirlem31  38489  poimir  38491  heicant  38493  voliunnfl  38502  volsupnfl  38503  itg2addnclem  38509  findcard4  38552  unirep  38568  sdclem2  38596  istotbnd3  38625  ssbnd  38642  eldisjlem19  39765  lshpdisj  39964  lsatn0  39976  lsat0cv  40010  cvrletrN  40250  cvrval4N  40391  lncvrelatN  40758  paddasslem14  40810  paddasslem15  40811  paddasslem16  40812  pmapjoin  40829  dihglblem2N  42271  dochvalr  42334  eqresfnbd  43206  sn-sup2  43483  prjspner1  43576  flt4lem7  43609  incssnn0  43660  eldioph4b  43756  diophren  43758  fphpdo  43762  rencldnfilem  43765  pellexlem5  43778  pell1234qrne0  43798  pell1234qrmulcl  43800  pell14qrgt0  43804  pell1234qrdich  43806  pell14qrdich  43814  pell1qrge1  43815  pell1qrgap  43819  pellfundre  43826  pellfundlb  43829  dvdsacongtr  43929  jm2.19lem4  43937  aomclem4  44002  hbtlem2  44069  hbtlem4  44071  hbtlem6  44074  cantnfresb  44269  dflim5  44274  tfsconcatrn  44287  tfsconcatrev  44293  naddwordnexlem4  44346  safesnsupfiss  44359  harval3  44482  clcnvlem  44567  relpfrlem  45880  cfsetsnfsetfo  48052  euoreqb  48101  2reu8i  48105  sprsymrelf1lem  48495  sprsymrelfolem2  48497  reupr  48526  fmtnofac2lem  48575  opoeALTV  48703  opeoALTV  48704  fpprwpprb  48760  gboge9  48784  clnbgrel  48848  grimco  48909  uhgrimedgi  48910  isuspgrim  48916  cycldlenngric  48948  uhgrimisgrgric  48951  clnbgrgrimlem  48953  clnbgrgrim  48954  grtriprop  48961  stgrusgra  48979  grlimedgclnbgr  49015  grlimprclnbgrvtx  49019  grlimgredgex  49020  grlictr  49035  gpgedg2iv  49087  gpgcubic  49099  gpg5nbgr3star  49101  pgnbgreunbgrlem2  49137  pgnbgreunbgrlem5  49143  ellcoellss  49469  nn0sumshdiglem1  49655  itschlc0xyqsol  49801  itsclc0  49805  opnneilv  49939