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  3163  disjiun  5091  reusv3  5367  euotd  5486  swopo  5570  sotr3  5600  wereu2  5648  poirr2  6118  sossfld  6178  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  8211  tposfo2  8266  wfr3g  8337  tz7.48-2  8452  omeulem1  8590  omeu  8593  nnaordex  8647  eldifsucnn  8673  pssnn  9184  onomeneq  9229  fodomfib  9320  dffi3  9423  supmo  9444  supnub  9454  infglb  9483  infnlb  9485  infmo  9489  infsupprpr  9498  cantnfle  9672  cantnflem1  9690  epfrs  9732  frr3g  9760  updjud  10015  alephord2i  10156  cardinfima  10176  aceq3lem  10199  dfac2b  10209  dfac12lem2  10223  axdc2lem  10526  ttukeylem6  10592  alephval2  10657  fpwwe2lem11  10726  fpwwe2lem12  10727  prlem934  11118  reclem4pr  11135  suplem1pr  11137  letr  11404  sup2  12273  uzind  12791  ledivge1le  13193  xrletr  13287  xltnegi  13346  xlemul1a  13418  ixxssixx  13490  difreicc  13615  flval3  13955  fsequb  14118  seqf1olem1  14184  expnegz  14239  hash2prd  14620  ccatrcl1  14741  relexprelg  15191  shftlem  15221  rexuzre  15520  cau3lem  15522  caubnd2  15525  caubnd  15526  climrlim2  15714  climuni  15719  2clim  15739  o1co  15753  rlimno1  15821  climbdd  15839  caurcvg  15844  summolem2  15882  summo  15883  zsum  15884  fsumf1o  15889  fsumss  15891  fsumcl2lem  15897  fsumadd  15906  fsummulc2  15950  fsumconst  15956  fsumrelem  15974  prodmolem2  16102  prodmo  16103  zprod  16104  fprodf1o  16113  fprodss  16115  fprodcl2lem  16117  fprodmul  16127  fproddiv  16128  fprodconst  16145  fprodn0  16146  dfgcd2  16719  lcmfunsnlem2  16815  coprmproddvdslem  16837  cncongrprm  16905  prmpwdvds  17082  infpnlem1  17088  1arith  17105  vdwapun  17152  vdwlem11  17169  vdwnnlem2  17174  ramz  17203  ramcl  17207  prmlem0  17283  firest  17603  catpropd  17883  initoid  18176  termoid  18177  initoeu2lem1  18189  pltnle  18510  pltletr  18515  pospo  18517  psss  18754  mgmn0plusgf  18827  isgrpid2  19187  f1omvdco2  19662  pgpfi  19819  frgpnabllem1  20087  gsumval3eu  20118  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  ablfaclem3  20303  dvdsrtr  20598  dvdsrmul1  20599  unitgrp  20613  domnmuln0  20961  lspsolvlem  21420  gsumfsum  21740  nzerooringczr  21786  obslbs  22036  gsummoncoe1  22626  pf1ind  22673  dmatscmcl  22818  scmatmulcl  22833  smatvscl  22839  mdetdiaglem  22913  matunitlindflem1  22994  cpmatinvcl  23035  mp2pm2mplem4  23127  cpmadugsumlemF  23194  eltg3  23280  tgidm  23298  neindisj  23435  tgrest  23477  restcld  23490  tgcn  23570  lmcnp  23622  iunconnlem  23745  2ndcredom  23768  2ndc1stc  23769  1stcrest  23771  2ndcrest  23772  2ndcdisj  23775  nllyrest  23805  nllyidm  23808  lfinpfin  23843  locfincmp  23845  ptpjpre1  23890  ptuni2  23895  ptbasin  23896  ptbasfi  23900  txbasval  23925  ptpjopn  23931  ptclsg  23934  dfac14lem  23936  xkoccn  23938  txcnp  23939  ptcnplem  23940  ptcnp  23941  txtube  23959  txcmplem1  23960  txcmplem2  23961  tx2ndc  23970  txkgen  23971  xkoco1cn  23976  xkoco2cn  23977  xkococnlem  23978  xkococn  23979  xkoinjcn  24006  qtoprest  24036  kqsat  24050  kqcldsat  24052  isfild  24177  fbunfip  24188  fgabs  24198  filconn  24202  fbasrn  24203  filufint  24239  elfm2  24267  elfm3  24269  fmfnfm  24277  hausflimi  24299  cnpflfi  24318  ptcmplem2  24372  tmdgsum2  24415  cldsubg  24430  qustgpopn  24439  ustfilxp  24532  bldisj  24717  xbln0  24733  blssps  24743  blss  24744  blssexps  24745  blssex  24746  blcls  24825  metcnp3  24859  icccmplem2  25143  mpomulcn  25188  cnheibor  25276  iscau4  25600  cmssmscld  25671  ovolshftlem2  25831  ovolicc2lem5  25842  dyadmax  25919  mbfi1fseqlem4  26039  mbfi1flimlem  26043  lhop1lem  26333  dvfsumrlim  26351  aalioulem3  26661  ulmcn  26726  radcnvlt1  26745  pilem2  26779  efopn  26986  cxpeq0  27006  cxpmul2z  27019  cxpcn3lem  27075  xrlimcnp  27296  vmappw  27443  fsumvma  27540  dchrptlem1  27591  lgsqr  27678  lgsdchrval  27681  2lgslem3  27731  2sqlem6  27750  2sqlem7  27751  2sqreultlem  27774  2sqreunnltlem  27777  pntlem3  27936  pntleml  27938  flt4lem7  27989  ltsval2  28013  nosupno  28060  nosupbnd1lem5  28069  noinfno  28075  lestr  28119  madebdayim  28274  ltslpss  28294  negsid  28427  noseqinds  28679  brbtwn  29477  brcgr  29478  axcontlem8  29549  nbumgrvtx  29927  cusgrfilem2  30037  1loopgrnb0  30083  uspgr2wlkeq  30226  wlklenvclwlk  30234  subgrwlk  30269  upgrwlkdvdelem  30322  uspgrn2crct  30397  0enwwlksnge1  30453  usgr2wspthons3  30556  clwwlkccatlem  30580  clwlkclwwlkf  30599  clwwlknonel  30686  frgrncvvdeqlem9  30908  frgr2wwlkeqm  30932  frgrreggt1  30994  frgrreg  30995  pjhthmo  31904  spansncvi  32254  nmcexi  32628  cnlnssadj  32682  leopmuli  32735  elpjrn  32792  mdsl0  32912  sumdmdii  33017  fmptcof2  33251  suppss3  33315  lmxrge0  34584  bnj594  35542  bnj849  35555  noinfepfnregs  35800  erdszelem7  35962  sconnpi1  36004  cvmsval  36031  cvmopnlem  36043  cvmfolem  36044  cvmliftmolem2  36047  cvmlift2lem10  36077  cvmlift2lem12  36079  cvmlift3lem5  36088  cvmlift3lem8  36091  satfv0  36123  satfv1  36128  satfvsucsuc  36130  satffunlem1lem2  36168  satffunlem2lem2  36171  linethru  36918  opnrebl2  37109  neibastop2lem  37148  neibastop2  37149  bj-cbv3ta  37698  cgsex2gd  38058  isinf2  38328  phpreu  38527  finixpnum  38528  lindsadd  38536  ptrecube  38538  poimirlem26  38564  poimirlem27  38565  poimirlem31  38569  poimir  38571  heicant  38573  voliunnfl  38582  volsupnfl  38583  itg2addnclem  38589  findcard4  38632  unirep  38648  sdclem2  38676  istotbnd3  38705  ssbnd  38722  eldisjlem19  39845  lshpdisj  40044  lsatn0  40056  lsat0cv  40090  cvrletrN  40330  cvrval4N  40471  lncvrelatN  40838  paddasslem14  40890  paddasslem15  40891  paddasslem16  40892  pmapjoin  40909  dihglblem2N  42351  dochvalr  42414  eqresfnbd  43286  sn-sup2  43555  incssnn0  43721  eldioph4b  43817  diophren  43819  fphpdo  43823  rencldnfilem  43826  pellexlem5  43839  pell1234qrne0  43859  pell1234qrmulcl  43861  pell14qrgt0  43865  pell1234qrdich  43867  pell14qrdich  43875  pell1qrge1  43876  pell1qrgap  43880  pellfundre  43887  pellfundlb  43890  dvdsacongtr  43990  jm2.19lem4  43998  aomclem4  44058  hbtlem2  44125  hbtlem4  44127  hbtlem6  44130  cantnfresb  44325  dflim5  44330  tfsconcatrn  44343  tfsconcatrev  44349  naddwordnexlem4  44402  safesnsupfiss  44415  harval3  44538  clcnvlem  44622  relpfrlem  45942  cfsetsnfsetfo  48129  euoreqb  48178  2reu8i  48182  sprsymrelf1lem  48572  sprsymrelfolem2  48574  reupr  48603  fmtnofac2lem  48652  opoeALTV  48780  opeoALTV  48781  fpprwpprb  48837  gboge9  48861  clnbgrel  48925  grimco  48986  uhgrimedgi  48987  isuspgrim  48993  cycldlenngric  49025  uhgrimisgrgric  49028  clnbgrgrimlem  49030  clnbgrgrim  49031  grtriprop  49038  stgrusgra  49056  grlimedgclnbgr  49092  grlimprclnbgrvtx  49096  grlimgredgex  49097  grlictr  49112  gpgedg2iv  49164  gpgcubic  49176  gpg5nbgr3star  49178  pgnbgreunbgrlem2  49214  pgnbgreunbgrlem5  49220  ellcoellss  49546  nn0sumshdiglem1  49732  itschlc0xyqsol  49878  itsclc0  49882  opnneilv  50016