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  5485  swopo  5569  sotr3  5599  wereu2  5647  poirr2  6117  sossfld  6177  reuop  6296  frpomin  6343  ordpss  6391  oneqmini  6416  suctr  6451  elpreima  7057  fmptco  7130  isofrlem  7348  onmindif2  7821  resf1extb  7946  mptcnfimad  7998  frxp  8138  fnse  8150  suppss  8212  tposfo2  8267  wfr3g  8338  tz7.48-2  8453  omeulem1  8591  omeu  8594  nnaordex  8648  eldifsucnn  8674  pssnn  9185  onomeneq  9230  fodomfib  9321  dffi3  9424  supmo  9445  supnub  9455  infglb  9484  infnlb  9486  infmo  9490  infsupprpr  9499  cantnfle  9673  cantnflem1  9691  epfrs  9733  frr3g  9761  updjud  10016  alephord2i  10157  cardinfima  10177  aceq3lem  10200  dfac2b  10210  dfac12lem2  10224  axdc2lem  10527  ttukeylem6  10593  alephval2  10658  fpwwe2lem11  10727  fpwwe2lem12  10728  prlem934  11119  reclem4pr  11136  suplem1pr  11138  letr  11405  sup2  12274  uzind  12792  ledivge1le  13194  xrletr  13288  xltnegi  13347  xlemul1a  13419  ixxssixx  13491  difreicc  13616  flval3  13956  fsequb  14119  seqf1olem1  14185  expnegz  14240  hash2prd  14621  ccatrcl1  14742  relexprelg  15192  shftlem  15222  rexuzre  15521  cau3lem  15523  caubnd2  15526  caubnd  15527  climrlim2  15715  climuni  15720  2clim  15740  o1co  15754  rlimno1  15822  climbdd  15840  caurcvg  15845  summolem2  15883  summo  15884  zsum  15885  fsumf1o  15890  fsumss  15892  fsumcl2lem  15898  fsumadd  15907  fsummulc2  15951  fsumconst  15957  fsumrelem  15975  prodmolem2  16103  prodmo  16104  zprod  16105  fprodf1o  16114  fprodss  16116  fprodcl2lem  16118  fprodmul  16128  fproddiv  16129  fprodconst  16146  fprodn0  16147  dfgcd2  16720  lcmfunsnlem2  16816  coprmproddvdslem  16838  cncongrprm  16906  prmpwdvds  17083  infpnlem1  17089  1arith  17106  vdwapun  17153  vdwlem11  17170  vdwnnlem2  17175  ramz  17204  ramcl  17208  prmlem0  17284  firest  17604  catpropd  17884  initoid  18177  termoid  18178  initoeu2lem1  18190  pltnle  18511  pltletr  18516  pospo  18518  psss  18755  mgmn0plusgf  18828  isgrpid2  19188  f1omvdco2  19663  pgpfi  19820  frgpnabllem1  20088  gsumval3eu  20119  gsumzres  20124  gsumzcl2  20125  gsumzf1o  20127  gsumzaddlem  20136  gsumconst  20149  gsumzmhm  20152  gsumzoppg  20159  ablfaclem3  20304  dvdsrtr  20599  dvdsrmul1  20600  unitgrp  20614  domnmuln0  20962  lspsolvlem  21421  gsumfsum  21741  nzerooringczr  21787  obslbs  22037  gsummoncoe1  22627  pf1ind  22674  dmatscmcl  22819  scmatmulcl  22834  smatvscl  22840  mdetdiaglem  22914  matunitlindflem1  22995  cpmatinvcl  23036  mp2pm2mplem4  23128  cpmadugsumlemF  23195  eltg3  23281  tgidm  23299  neindisj  23436  tgrest  23478  restcld  23491  tgcn  23571  lmcnp  23623  iunconnlem  23746  2ndcredom  23769  2ndc1stc  23770  1stcrest  23772  2ndcrest  23773  2ndcdisj  23776  nllyrest  23806  nllyidm  23809  lfinpfin  23844  locfincmp  23846  ptpjpre1  23891  ptuni2  23896  ptbasin  23897  ptbasfi  23901  txbasval  23926  ptpjopn  23932  ptclsg  23935  dfac14lem  23937  xkoccn  23939  txcnp  23940  ptcnplem  23941  ptcnp  23942  txtube  23960  txcmplem1  23961  txcmplem2  23962  tx2ndc  23971  txkgen  23972  xkoco1cn  23977  xkoco2cn  23978  xkococnlem  23979  xkococn  23980  xkoinjcn  24007  qtoprest  24037  kqsat  24051  kqcldsat  24053  isfild  24178  fbunfip  24189  fgabs  24199  filconn  24203  fbasrn  24204  filufint  24240  elfm2  24268  elfm3  24270  fmfnfm  24278  hausflimi  24300  cnpflfi  24319  ptcmplem2  24373  tmdgsum2  24416  cldsubg  24431  qustgpopn  24440  ustfilxp  24533  bldisj  24718  xbln0  24734  blssps  24744  blss  24745  blssexps  24746  blssex  24747  blcls  24826  metcnp3  24860  icccmplem2  25144  mpomulcn  25189  cnheibor  25277  iscau4  25601  cmssmscld  25672  ovolshftlem2  25832  ovolicc2lem5  25843  dyadmax  25920  mbfi1fseqlem4  26040  mbfi1flimlem  26044  lhop1lem  26334  dvfsumrlim  26352  aalioulem3  26662  ulmcn  26727  radcnvlt1  26746  pilem2  26780  efopn  26987  cxpeq0  27007  cxpmul2z  27020  cxpcn3lem  27076  xrlimcnp  27297  vmappw  27444  fsumvma  27541  dchrptlem1  27592  lgsqr  27679  lgsdchrval  27682  2lgslem3  27732  2sqlem6  27751  2sqlem7  27752  2sqreultlem  27775  2sqreunnltlem  27778  pntlem3  27937  pntleml  27939  flt4lem7  27990  ltsval2  28014  nosupno  28061  nosupbnd1lem5  28070  noinfno  28076  lestr  28120  madebdayim  28275  ltslpss  28295  negsid  28428  noseqinds  28680  brbtwn  29478  brcgr  29479  axcontlem8  29550  nbumgrvtx  29928  cusgrfilem2  30038  1loopgrnb0  30084  uspgr2wlkeq  30227  wlklenvclwlk  30235  subgrwlk  30270  upgrwlkdvdelem  30323  uspgrn2crct  30398  0enwwlksnge1  30454  usgr2wspthons3  30557  clwwlkccatlem  30581  clwlkclwwlkf  30600  clwwlknonel  30687  frgrncvvdeqlem9  30909  frgr2wwlkeqm  30933  frgrreggt1  30995  frgrreg  30996  pjhthmo  31905  spansncvi  32255  nmcexi  32629  cnlnssadj  32683  leopmuli  32736  elpjrn  32793  mdsl0  32913  sumdmdii  33018  fmptcof2  33294  suppss3  33358  lmxrge0  34627  bnj594  35585  bnj849  35598  noinfepfnregs  35849  erdszelem7  36031  sconnpi1  36073  cvmsval  36100  cvmopnlem  36112  cvmfolem  36113  cvmliftmolem2  36116  cvmlift2lem10  36146  cvmlift2lem12  36148  cvmlift3lem5  36157  cvmlift3lem8  36160  satfv0  36192  satfv1  36197  satfvsucsuc  36199  satffunlem1lem2  36237  satffunlem2lem2  36240  linethru  36993  opnrebl2  37184  neibastop2lem  37223  neibastop2  37224  bj-cbv3ta  37773  cgsex2gd  38134  isinf2  38404  phpreu  38603  finixpnum  38604  lindsadd  38612  ptrecube  38614  poimirlem26  38640  poimirlem27  38641  poimirlem31  38645  poimir  38647  heicant  38649  voliunnfl  38658  volsupnfl  38659  itg2addnclem  38665  findcard4  38708  unirep  38724  sdclem2  38752  istotbnd3  38781  ssbnd  38798  eldisjlem19  39921  lshpdisj  40120  lsatn0  40132  lsat0cv  40166  cvrletrN  40406  cvrval4N  40547  lncvrelatN  40914  paddasslem14  40966  paddasslem15  40967  paddasslem16  40968  pmapjoin  40985  dihglblem2N  42427  dochvalr  42490  eqresfnbd  43362  sn-sup2  43631  incssnn0  43798  eldioph4b  43894  diophren  43896  fphpdo  43900  rencldnfilem  43903  pellexlem5  43916  pell1234qrne0  43936  pell1234qrmulcl  43938  pell14qrgt0  43942  pell1234qrdich  43944  pell14qrdich  43952  pell1qrge1  43953  pell1qrgap  43957  pellfundre  43964  pellfundlb  43967  dvdsacongtr  44067  jm2.19lem4  44075  aomclem4  44135  hbtlem2  44202  hbtlem4  44204  hbtlem6  44207  cantnfresb  44402  dflim5  44407  tfsconcatrn  44420  tfsconcatrev  44426  naddwordnexlem4  44479  safesnsupfiss  44492  harval3  44615  clcnvlem  44699  relpfrlem  46019  cfsetsnfsetfo  48206  euoreqb  48255  2reu8i  48259  sprsymrelf1lem  48649  sprsymrelfolem2  48651  reupr  48680  fmtnofac2lem  48729  opoeALTV  48857  opeoALTV  48858  fpprwpprb  48914  gboge9  48938  clnbgrel  49002  grimco  49063  uhgrimedgi  49064  isuspgrim  49070  cycldlenngric  49102  uhgrimisgrgric  49105  clnbgrgrimlem  49107  clnbgrgrim  49108  grtriprop  49115  stgrusgra  49133  grlimedgclnbgr  49169  grlimprclnbgrvtx  49173  grlimgredgex  49174  grlictr  49189  gpgedg2iv  49241  gpgcubic  49253  gpg5nbgr3star  49255  pgnbgreunbgrlem2  49291  pgnbgreunbgrlem5  49297  ellcoellss  49623  nn0sumshdiglem1  49809  itschlc0xyqsol  49955  itsclc0  49959  opnneilv  50093