Theorem expimpd 457

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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 414	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ornld  1057  3impia  1114  ralrimdva  3154  disjiun  5017  reusv3  5271  euotd  5368  swopo  5448  wereu2  5516  poirr2  5951  sossfld  6010  reuop  6112  oneqmini  6210  suctr  6242  elpreima  6805  fmptco  6868  isofrlem  7072  onmindif2  7507  frxp  7803  fnse  7810  suppss  7843  tposfo2  7898  wfr3g  7936  tz7.48-2  8061  omeulem1  8191  omeu  8194  nnaordex  8247  pssnn  8720  fodomfib  8782  dffi3  8879  supmo  8900  supnub  8910  infglb  8938  infnlb  8940  infmo  8943  infsupprpr  8952  cantnfle  9118  cantnflem1  9136  epfrs  9157  updjud  9347  alephord2i  9488  cardinfima  9508  aceq3lem  9531  dfac2b  9541  dfac12lem2  9555  axdc2lem  9859  ttukeylem6  9925  alephval2  9983  fpwwe2lem12  10052  fpwwe2lem13  10053  prlem934  10444  reclem4pr  10461  suplem1pr  10463  letr  10723  sup2  11584  uzind  12062  ledivge1le  12448  xrletr  12539  xltnegi  12597  xlemul1a  12669  ixxssixx  12740  difreicc  12862  flval3  13180  fsequb  13338  seqf1olem1  13405  expnegz  13459  hash2prd  13829  ccatrcl1  13939  relexprelg  14389  shftlem  14419  rexuzre  14704  cau3lem  14706  caubnd2  14709  caubnd  14710  climrlim2  14896  climuni  14901  2clim  14921  o1co  14935  rlimno1  15002  climbdd  15020  caurcvg  15025  summolem2  15065  summo  15066  zsum  15067  fsumf1o  15072  fsumss  15074  fsumcl2lem  15080  fsumadd  15088  fsummulc2  15131  fsumconst  15137  fsumrelem  15154  prodmolem2  15281  prodmo  15282  zprod  15283  fprodf1o  15292  fprodss  15294  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodconst  15324  fprodn0  15325  dfgcd2  15884  lcmfunsnlem2  15974  coprmproddvdslem  15996  cncongrprm  16059  prmpwdvds  16230  infpnlem1  16236  1arith  16253  vdwapun  16300  vdwlem11  16317  vdwnnlem2  16322  ramz  16351  ramcl  16355  prmlem0  16431  firest  16698  catpropd  16971  initoid  17257  termoid  17258  initoeu2lem1  17266  pltnle  17568  pltletr  17573  pospo  17575  psss  17816  isgrpid2  18132  f1omvdco2  18568  pgpfi  18722  frgpnabllem1  18986  gsumval3eu  19017  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  ablfaclem3  19202  dvdsrtr  19398  dvdsrmul1  19399  unitgrp  19413  lspsolvlem  19907  domnmuln0  20064  gsumfsum  20158  obslbs  20419  gsummoncoe1  20933  pf1ind  20979  dmatscmcl  21108  scmatmulcl  21123  smatvscl  21129  mdetdiaglem  21203  cpmatinvcl  21322  mp2pm2mplem4  21414  cpmadugsumlemF  21481  eltg3  21567  tgidm  21585  neindisj  21722  tgrest  21764  restcld  21777  tgcn  21857  lmcnp  21909  iunconnlem  22032  2ndcredom  22055  2ndc1stc  22056  1stcrest  22058  2ndcrest  22059  2ndcdisj  22061  nllyrest  22091  nllyidm  22094  lfinpfin  22129  locfincmp  22131  ptpjpre1  22176  ptuni2  22181  ptbasin  22182  ptbasfi  22186  txbasval  22211  ptpjopn  22217  ptclsg  22220  dfac14lem  22222  xkoccn  22224  txcnp  22225  ptcnplem  22226  ptcnp  22227  txtube  22245  txcmplem1  22246  txcmplem2  22247  tx2ndc  22256  txkgen  22257  xkoco1cn  22262  xkoco2cn  22263  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  qtoprest  22322  kqsat  22336  kqcldsat  22338  isfild  22463  fbunfip  22474  fgabs  22484  filconn  22488  fbasrn  22489  filufint  22525  elfm2  22553  elfm3  22555  fmfnfm  22563  hausflimi  22585  cnpflfi  22604  ptcmplem2  22658  tmdgsum2  22701  cldsubg  22716  qustgpopn  22725  ustfilxp  22818  bldisj  23005  xbln0  23021  blssps  23031  blss  23032  blssexps  23033  blssex  23034  blcls  23113  metcnp3  23147  icccmplem2  23428  cnheibor  23560  iscau4  23883  cmssmscld  23954  ovolshftlem2  24114  ovolicc2lem5  24125  dyadmax  24202  mbfi1fseqlem4  24322  mbfi1flimlem  24326  lhop1lem  24616  dvfsumrlim  24634  aalioulem3  24930  ulmcn  24994  radcnvlt1  25013  pilem2  25047  efopn  25249  cxpeq0  25269  cxpmul2z  25282  cxpcn3lem  25336  xrlimcnp  25554  vmappw  25701  fsumvma  25797  dchrptlem1  25848  lgsqr  25935  lgsdchrval  25938  2lgslem3  25988  2sqlem6  26007  2sqlem7  26008  2sqreultlem  26031  2sqreunnltlem  26034  pntlem3  26193  pntleml  26195  brbtwn  26693  brcgr  26694  axcontlem8  26765  nbumgrvtx  27136  cusgrfilem2  27246  1loopgrnb0  27292  uspgr2wlkeq  27435  wlklenvclwlk  27444  upgrwlkdvdelem  27525  uspgrn2crct  27594  0enwwlksnge1  27650  usgr2wspthons3  27750  clwwlkccatlem  27774  clwlkclwwlkf  27793  clwwlknonel  27880  frgrncvvdeqlem9  28092  frgr2wwlkeqm  28116  frgrreggt1  28178  frgrreg  28179  pjhthmo  29085  spansncvi  29435  nmcexi  29809  cnlnssadj  29863  leopmuli  29916  elpjrn  29973  mdsl0  30093  sumdmdii  30198  fmptcof2  30420  suppss3  30486  lmxrge0  31305  bnj594  32294  bnj849  32307  subgrwlk  32492  erdszelem7  32557  sconnpi1  32599  cvmsval  32626  cvmopnlem  32638  cvmfolem  32639  cvmliftmolem2  32642  cvmlift2lem10  32672  cvmlift2lem12  32674  cvmlift3lem5  32683  cvmlift3lem8  32686  satfv0  32718  satfv1  32723  satfvsucsuc  32725  satffunlem1lem2  32763  satffunlem2lem2  32766  sotr3  33115  trpredrec  33190  frpomin  33191  frr3g  33234  sltval2  33276  nosupno  33316  nosupbnd1lem5  33325  sletr  33350  linethru  33727  opnrebl2  33782  neibastop2lem  33821  neibastop2  33822  bj-cbv3ta  34223  isinf2  34822  phpreu  35041  finixpnum  35042  lindsadd  35050  matunitlindflem1  35053  ptrecube  35057  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  poimir  35090  heicant  35092  voliunnfl  35101  volsupnfl  35102  itg2addnclem  35108  unirep  35151  sdclem2  35180  istotbnd3  35209  ssbnd  35226  lshpdisj  36283  lsatn0  36295  lsat0cv  36329  cvrletrN  36569  cvrval4N  36710  lncvrelatN  37077  paddasslem14  37129  paddasslem15  37130  paddasslem16  37131  pmapjoin  37148  dihglblem2N  38590  dochvalr  38653  sn-negex12  39553  sn-sup2  39594  incssnn0  39652  eldioph4b  39752  diophren  39754  fphpdo  39758  rencldnfilem  39761  pellexlem5  39774  pell1234qrne0  39794  pell1234qrmulcl  39796  pell14qrgt0  39800  pell1234qrdich  39802  pell14qrdich  39810  pell1qrge1  39811  pell1qrgap  39815  pellfundre  39822  pellfundlb  39825  dvdsacongtr  39925  jm2.19lem4  39933  aomclem4  40001  hbtlem2  40068  hbtlem4  40070  hbtlem6  40073  harval3  40244  clcnvlem  40323  ordpss  41155  euoreqb  43665  2reu8i  43669  sprsymrelf1lem  44008  sprsymrelfolem2  44010  reupr  44039  fmtnofac2lem  44085  opoeALTV  44201  opeoALTV  44202  fpprwpprb  44258  gboge9  44282  nzerooringczr  44696  ellcoellss  44844  nn0sumshdiglem1  45035  itschlc0xyqsol  45181  itsclc0  45185