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

This theorem is referenced by:  ornld  1059  3impia  1116  ralrimdva  3153  disjiun  5135  reusv3  5403  euotd  5513  swopo  5599  sotr3  5627  wereu2  5673  poirr2  6125  sossfld  6185  reuop  6292  frpomin  6341  oneqmini  6416  suctr  6450  elpreima  7059  fmptco  7129  isofrlem  7340  onmindif2  7799  frxp  8117  fnse  8124  suppss  8184  suppssOLD  8185  tposfo2  8240  wfr3g  8313  tz7.48-2  8448  omeulem1  8588  omeu  8591  nnaordex  8644  eldifsucnn  8669  pssnn  9174  onomeneq  9234  pssnnOLD  9271  fodomfib  9332  dffi3  9432  supmo  9453  supnub  9463  infglb  9491  infnlb  9493  infmo  9496  infsupprpr  9505  cantnfle  9672  cantnflem1  9690  epfrs  9732  frr3g  9757  updjud  9935  alephord2i  10078  cardinfima  10098  aceq3lem  10121  dfac2b  10131  dfac12lem2  10145  axdc2lem  10449  ttukeylem6  10515  alephval2  10573  fpwwe2lem11  10642  fpwwe2lem12  10643  prlem934  11034  reclem4pr  11051  suplem1pr  11053  letr  11315  sup2  12177  uzind  12661  ledivge1le  13052  xrletr  13144  xltnegi  13202  xlemul1a  13274  ixxssixx  13345  difreicc  13468  flval3  13787  fsequb  13947  seqf1olem1  14014  expnegz  14069  hash2prd  14443  ccatrcl1  14551  relexprelg  14992  shftlem  15022  rexuzre  15306  cau3lem  15308  caubnd2  15311  caubnd  15312  climrlim2  15498  climuni  15503  2clim  15523  o1co  15537  rlimno1  15607  climbdd  15625  caurcvg  15630  summolem2  15669  summo  15670  zsum  15671  fsumf1o  15676  fsumss  15678  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumconst  15743  fsumrelem  15760  prodmolem2  15886  prodmo  15887  zprod  15888  fprodf1o  15897  fprodss  15899  fprodcl2lem  15901  fprodmul  15911  fproddiv  15912  fprodconst  15929  fprodn0  15930  dfgcd2  16495  lcmfunsnlem2  16584  coprmproddvdslem  16606  cncongrprm  16672  prmpwdvds  16844  infpnlem1  16850  1arith  16867  vdwapun  16914  vdwlem11  16931  vdwnnlem2  16936  ramz  16965  ramcl  16969  prmlem0  17046  firest  17385  catpropd  17660  initoid  17961  termoid  17962  initoeu2lem1  17974  pltnle  18301  pltletr  18306  pospo  18308  psss  18543  isgrpid2  18904  f1omvdco2  19364  pgpfi  19521  frgpnabllem1  19789  gsumval3eu  19820  gsumzres  19825  gsumzcl2  19826  gsumzf1o  19828  gsumzaddlem  19837  gsumconst  19850  gsumzmhm  19853  gsumzoppg  19860  ablfaclem3  20005  dvdsrtr  20266  dvdsrmul1  20267  unitgrp  20281  lspsolvlem  20989  domnmuln0  21204  gsumfsum  21302  nzerooringczr  21341  obslbs  21596  gsummoncoe1  22149  pf1ind  22195  dmatscmcl  22326  scmatmulcl  22341  smatvscl  22347  mdetdiaglem  22421  cpmatinvcl  22540  mp2pm2mplem4  22632  cpmadugsumlemF  22699  eltg3  22786  tgidm  22804  neindisj  22942  tgrest  22984  restcld  22997  tgcn  23077  lmcnp  23129  iunconnlem  23252  2ndcredom  23275  2ndc1stc  23276  1stcrest  23278  2ndcrest  23279  2ndcdisj  23281  nllyrest  23311  nllyidm  23314  lfinpfin  23349  locfincmp  23351  ptpjpre1  23396  ptuni2  23401  ptbasin  23402  ptbasfi  23406  txbasval  23431  ptpjopn  23437  ptclsg  23440  dfac14lem  23442  xkoccn  23444  txcnp  23445  ptcnplem  23446  ptcnp  23447  txtube  23465  txcmplem1  23466  txcmplem2  23467  tx2ndc  23476  txkgen  23477  xkoco1cn  23482  xkoco2cn  23483  xkococnlem  23484  xkococn  23485  xkoinjcn  23512  qtoprest  23542  kqsat  23556  kqcldsat  23558  isfild  23683  fbunfip  23694  fgabs  23704  filconn  23708  fbasrn  23709  filufint  23745  elfm2  23773  elfm3  23775  fmfnfm  23783  hausflimi  23805  cnpflfi  23824  ptcmplem2  23878  tmdgsum2  23921  cldsubg  23936  qustgpopn  23945  ustfilxp  24038  bldisj  24225  xbln0  24241  blssps  24251  blss  24252  blssexps  24253  blssex  24254  blcls  24336  metcnp3  24370  icccmplem2  24660  mpomulcn  24706  cnheibor  24802  iscau4  25128  cmssmscld  25199  ovolshftlem2  25360  ovolicc2lem5  25371  dyadmax  25448  mbfi1fseqlem4  25569  mbfi1flimlem  25573  lhop1lem  25867  dvfsumrlim  25887  aalioulem3  26187  ulmcn  26251  radcnvlt1  26270  pilem2  26305  efopn  26507  cxpeq0  26527  cxpmul2z  26540  cxpcn3lem  26597  xrlimcnp  26815  vmappw  26963  fsumvma  27061  dchrptlem1  27112  lgsqr  27199  lgsdchrval  27202  2lgslem3  27252  2sqlem6  27271  2sqlem7  27272  2sqreultlem  27295  2sqreunnltlem  27298  pntlem3  27457  pntleml  27459  sltval2  27504  nosupno  27551  nosupbnd1lem5  27560  noinfno  27566  sletr  27606  madebdayim  27729  sltlpss  27748  negsid  27868  brbtwn  28592  brcgr  28593  axcontlem8  28664  nbumgrvtx  29038  cusgrfilem2  29148  1loopgrnb0  29194  uspgr2wlkeq  29338  wlklenvclwlk  29347  upgrwlkdvdelem  29428  uspgrn2crct  29497  0enwwlksnge1  29553  usgr2wspthons3  29653  clwwlkccatlem  29677  clwlkclwwlkf  29696  clwwlknonel  29783  frgrncvvdeqlem9  29995  frgr2wwlkeqm  30019  frgrreggt1  30081  frgrreg  30082  pjhthmo  30990  spansncvi  31340  nmcexi  31714  cnlnssadj  31768  leopmuli  31821  elpjrn  31878  mdsl0  31998  sumdmdii  32103  fmptcof2  32317  suppss3  32384  lmxrge0  33398  bnj594  34389  bnj849  34402  subgrwlk  34589  erdszelem7  34654  sconnpi1  34696  cvmsval  34723  cvmopnlem  34735  cvmfolem  34736  cvmliftmolem2  34739  cvmlift2lem10  34769  cvmlift2lem12  34771  cvmlift3lem5  34780  cvmlift3lem8  34783  satfv0  34815  satfv1  34820  satfvsucsuc  34822  satffunlem1lem2  34860  satffunlem2lem2  34863  linethru  35597  opnrebl2  35673  neibastop2lem  35712  neibastop2  35713  bj-cbv3ta  36131  isinf2  36753  phpreu  36939  finixpnum  36940  lindsadd  36948  matunitlindflem1  36951  ptrecube  36955  poimirlem26  36981  poimirlem27  36982  poimirlem31  36986  poimir  36988  heicant  36990  voliunnfl  36999  volsupnfl  37000  itg2addnclem  37006  unirep  37049  sdclem2  37077  istotbnd3  37106  ssbnd  37123  eldisjlem19  38147  lshpdisj  38324  lsatn0  38336  lsat0cv  38370  cvrletrN  38610  cvrval4N  38752  lncvrelatN  39119  paddasslem14  39171  paddasslem15  39172  paddasslem16  39173  pmapjoin  39190  dihglblem2N  40632  dochvalr  40695  eqresfnbd  41524  sn-negex12  41755  sn-sup2  41808  prjspner1  41834  flt4lem7  41867  incssnn0  41915  eldioph4b  42015  diophren  42017  fphpdo  42021  rencldnfilem  42024  pellexlem5  42037  pell1234qrne0  42057  pell1234qrmulcl  42059  pell14qrgt0  42063  pell1234qrdich  42065  pell14qrdich  42073  pell1qrge1  42074  pell1qrgap  42078  pellfundre  42085  pellfundlb  42088  dvdsacongtr  42189  jm2.19lem4  42197  aomclem4  42265  hbtlem2  42332  hbtlem4  42334  hbtlem6  42337  cantnfresb  42540  dflim5  42545  tfsconcatrn  42558  tfsconcatrev  42564  naddwordnexlem4  42618  safesnsupfiss  42632  harval3  42755  clcnvlem  42840  ordpss  43676  cfsetsnfsetfo  46232  euoreqb  46279  2reu8i  46283  sprsymrelf1lem  46621  sprsymrelfolem2  46623  reupr  46652  fmtnofac2lem  46698  opoeALTV  46813  opeoALTV  46814  fpprwpprb  46870  gboge9  46894  ellcoellss  47281  nn0sumshdiglem1  47472  itschlc0xyqsol  47618  itsclc0  47622  opnneilv  47706