Theorem expr 461

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
expr	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 425	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 411	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  animpimp2impd  859  3expia  1137  rexlimdvaa  3173  reximddv  3187  disjxiun  5110  wereu2  5659  frpomin  6342  ordtr3  6408  fcof1  7286  knatar  7356  riota5f  7396  ovmpodf  7567  extmptsuppeq  8184  suppss  8190  suppss2  8196  frrlem14  8296  fprresex  8307  smoord  8352  tfrlem9a  8373  oaass  8546  oelimcl  8586  oaabs2  8635  cofon1  8658  naddssim  8672  swoso  8729  eceqoveq  8820  domdifsn  9048  domunsncan  9065  omxpenlem  9066  enfixsn  9074  mapdom2  9136  frfi  9245  fofinf1o  9289  finsschain  9316  elfiun  9390  marypha1lem  9393  eqsupd  9417  eqinfd  9446  ordiso2  9477  ordtypelem6  9485  ordtypelem7  9486  ordtypelem10  9489  oismo  9502  wemapsolem  9512  brwdom2  9535  wdomtr  9537  unwdomg  9546  xpwdomg  9547  unxpwdom2  9550  cantnfval2  9638  cantnfle  9640  cantnflem1  9658  cantnf  9662  r1ordg  9750  tcrank  9856  carddomi2  9956  harval2  9983  infxpenlem  9997  infxpenc2lem2  10004  fseqenlem1  10008  dfac8clem  10016  acndom2  10038  infpwfien  10046  iunfictbso  10098  dfac12lem3  10129  infxp  10197  coflim  10245  cofsmo  10253  coftr  10257  sornom  10261  infpssrlem4  10290  enfin2i  10305  fin23lem26  10309  fin23lem27  10312  fin23lem36  10332  fin23lem40  10335  isf32lem5  10341  isf34lem4  10361  isfin1-3  10370  fin1a2lem10  10393  fin1a2lem13  10396  fin1a2s  10398  hsmexlem4  10413  ttukeylem5  10497  ttukeylem6  10498  ttukeylem7  10499  alephval2  10557  gchor  10612  fpwwe2lem6  10621  fpwwe2lem11  10626  fpwwe2  10628  pwfseqlem4a  10646  pwfseqlem4  10647  winalim2  10681  gchina  10684  inar1  10760  nqereq  10920  prlem934  11018  prlem936  11032  addsrmo  11058  mulsrmo  11059  supsrlem  11096  axpre-sup  11154  dedekind  11373  dedekindle  11374  mulge0b  12085  supaddc  12182  supmul1  12184  un0addcl  12537  un0mulcl  12538  uzwo3  12967  qbtwnre  13225  xlemul1a  13314  seqcl2  14056  seqfveq2  14060  seqshft2  14064  monoord  14068  seqsplit  14071  seqf1olem1  14077  seqid2  14084  seqhomo  14085  expnegz  14132  expcan  14205  ltexp2  14206  discr  14276  bcval5  14354  hashbc  14490  hashf1lem2  14493  seqcoll  14501  seqcoll2  14502  wrdind  14759  wrd2ind  14760  sgn3da  15138  cau3lem  15406  ello1d  15574  lo1bdd2  15575  rlimclim  15597  climrlim2  15598  rlimdm  15602  rlimcn1  15639  reccn2  15648  rlimsqzlem  15700  lo1le  15703  caucvgrlem  15724  caurcvg2  15729  summolem2  15767  zsum  15769  fsum  15771  fsumf1o  15774  sumss  15775  fsumss  15776  fsumcl2lem  15782  fsumadd  15791  fsumcom2  15825  fsum0diag2  15834  fsummulc2  15835  fsumconst  15841  fsumrelem  15859  fsumrlim  15863  fsumo1  15864  divrcnv  15906  geomulcvg  15930  mertenslem2  15939  prodmolem2  15989  zprod  15991  fprod  15995  fprodf1o  16000  prodss  16001  fprodss  16002  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodconst  16032  fprodn0  16033  fprodcom2  16038  ruclem8  16293  dvds0lem  16324  dvdsnegb  16331  dvdssub2  16359  bitsf1  16504  bitsshft  16533  bezoutlem3  16599  bezoutlem4  16600  isprm5  16766  isprm6  16773  hashgcdeq  16849  modprminv  16859  modprminveq  16860  reumodprminv  16864  pcqmul  16913  pcqcl  16916  pcxnn0cl  16920  pcxcl  16921  pc2dvds  16939  pcadd  16949  pcmpt  16952  pockthg  16966  infpnlem1  16970  prmreclem5  16980  vdwlem2  17042  vdwlem9  17049  vdwlem10  17050  vdwlem12  17052  ramub  17073  0ram  17080  ramub1lem2  17087  ramub1  17088  ramcl  17089  mreexexd  17704  acsfn2  17719  iscatd  17729  catpropd  17765  setcmon  18144  pleval2i  18390  psss  18636  mgmidsssn0  18730  mgmhmeql  18774  mhmeql  18885  frmdss2  18922  frmdup3  18926  grprcan  19040  dfgrp3lem  19104  mulgnn0ass  19176  isnsg3  19226  ghmpreima  19308  ghmeql  19309  gaorber  19378  f1omvdco2  19518  psgnunilem1  19563  psgnunilem2  19565  oddvds  19617  gexdvds  19654  sylow1lem1  19668  odcau  19674  pgpssslw  19684  sylow2alem2  19688  sylow2blem3  19692  fislw  19695  lsmmod  19745  efgredlem  19817  frgpup3  19848  gsumval3  19977  gsumzres  19979  gsumzcl2  19980  gsumzf1o  19982  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  gsumzoppg  20014  gsum2d2lem  20043  ablfac1eulem  20144  pgpfac1lem5  20151  ablfaclem3  20159  issubdrg  20861  lss1d  21062  lmhmeql  21154  lspextmo  21155  lspsnat  21247  lsppratlem6  21254  islbs3  21257  lbsextlem4  21263  lidl1el  21329  cnsubrg  21546  gsumfsum  21553  prmirredlem  21591  znidomb  21680  frgpcyg  21692  cssmre  21812  dsmmsubg  21862  dsmmlss  21863  frlmsslsp  21915  lindff1  21939  lindfrn  21940  rnasclassa  22014  mvrf1  22104  mplsubglem  22117  mpllsslem  22118  mplcoe1  22157  mplcoe5  22160  gsummoncoe1  22437  mat1dimcrng  22603  mdetdiaglem  22724  mdetunilem7  22744  mdetunilem8  22745  mdetunilem9  22746  cpmatacl  22842  cpmatmcllem  22844  mp2pm2mplem4  22935  en2top  23111  toponmre  23219  topssnei  23250  innei  23251  clslp  23274  restcls  23307  restntr  23308  ordtrest2lem  23329  cnpco  23393  cncls2  23399  cncnpi  23404  cncnp  23406  cnconst2  23409  cnpdis  23419  lmcnp  23430  cnhaus  23480  isreg2  23503  cncmp  23518  tgcmp  23527  sscmp  23531  cmpfi  23534  cnconn  23548  iunconnlem  23553  clsconn  23556  1stcfb  23571  1stcrest  23579  2ndcctbss  23581  2ndcdisj  23582  1stcelcls  23587  1stccnp  23588  restnlly  23608  cldllycmp  23621  lly1stc  23622  dislly  23623  locfincmp  23652  comppfsc  23658  kgentopon  23664  kgenidm  23673  1stckgenlem  23679  kgencn3  23684  ptpjpre1  23697  ptbasin  23703  txcls  23730  tx2cn  23736  ptpjcn  23737  ptclsg  23741  ptcnp  23748  txdis  23758  txlly  23762  txnlly  23763  pthaus  23764  txtube  23766  txcmplem1  23767  txcmplem2  23768  txcmp  23769  txhaus  23773  txkgen  23778  xkohaus  23779  xkococnlem  23785  xkococn  23786  txconn  23815  qtopeu  23842  qtoprest  23843  regr1lem2  23866  kqreglem1  23867  cmphaushmeo  23926  xkocnv  23940  fgabs  24005  filuni  24011  trufil  24036  ufileu  24045  filufint  24046  fin1aufil  24058  elfm2  24074  rnelfmlem  24078  fmfnfmlem2  24081  fmfnfmlem4  24083  fmufil  24085  flimopn  24101  fbflim2  24103  hausflimi  24106  hausflim  24107  flimcf  24108  flimclslem  24110  flimsncls  24112  hauspwpwf1  24113  cnpflfi  24125  fclsnei  24145  fclscf  24151  flimfnfcls  24154  fclscmp  24156  ufilcmp  24158  fcfnei  24161  cnpfcf  24167  alexsublem  24170  alexsub  24171  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  ptcmplem3  24180  ptcmplem4  24181  ptcmplem5  24182  symgtgp  24232  tgpconncompeqg  24238  tgpconncomp  24239  ghmcnp  24241  tgpt0  24245  qustgplem  24247  haustsms2  24263  tsmsgsum  24265  tsmsres  24270  tsmsxp  24281  imasdsf1olem  24499  xbln0  24540  blssps  24550  blss  24551  neibl  24627  blcld  24631  metss  24634  metequiv2  24636  met1stc  24647  metrest  24650  prdsxmslem2  24655  metcnp3  24666  nrmmetd  24700  nlmvscnlem1  24812  nrginvrcnlem  24817  nmoleub  24857  icccmplem2  24950  icccmp  24952  reconnlem2  24954  xrge0tsms  24961  metdstri  24978  metdseq0  24981  metdscn  24983  cnmpopc  25056  lebnumlem3  25091  pcoval2  25144  pcopt  25150  nmoleub2lem  25242  nmhmcn  25248  ipcnlem1  25373  cfilfcls  25402  cmetcaulem  25416  iscmet3lem2  25420  iscmet3  25421  equivcau  25428  caubl  25436  bcthlem2  25453  bcthlem3  25454  bcthlem4  25455  bcthlem5  25456  ivthlem2  25580  ivthlem3  25581  ovoliunlem2  25631  ovolicc2lem2  25646  ovolicc2lem5  25649  ovolicc2  25650  ismbl2  25655  nulmbl  25663  nulmbl2  25664  unmbl  25665  shftmbl  25666  voliunlem3  25680  volsup  25684  ioombl1lem4  25689  ioombl1  25690  icombl  25692  ioombl  25693  uniioombl  25717  opnmbllem  25729  volivth  25735  vitali  25741  mbflimsup  25794  i1fadd  25823  itg1addlem4  25827  itg2le  25867  itg2seq  25870  itg2lea  25872  itg2splitlem  25876  itg2split  25877  itg2mono  25881  itg2gt0  25888  itg2cnlem2  25890  itgss  25940  itgfsum  25955  itgcn  25973  ellimc3  26007  limcco  26021  limciun  26022  dvnres  26059  dvnfre  26080  rolle  26118  c1liplem1  26124  dvivth  26138  dvne0  26139  lhop1lem  26141  lhop1  26142  lhop  26144  dvcnvrelem1  26145  dvfsumrlim  26159  dvfsum2  26162  ftc1a  26165  ftc1lem6  26169  itgsubst  26177  tdeglem4  26186  mdegaddle  26200  mdegvscale  26201  mdegmullem  26204  deg1tmle  26244  ply1divex  26263  dvdsq1p  26289  fta1g  26296  fta1b  26298  plyco0  26318  coeeulem  26350  dgrlem  26355  plyco  26367  coemullem  26376  dgreq0  26391  dgrco  26401  plydivex  26427  quotcan  26439  aannenlem1  26458  aalioulem2  26463  aalioulem3  26464  taylthlem1  26502  ulmbdd  26527  itgulm  26537  radcnvlt1  26547  psercnlem1  26554  abelthlem2  26561  abelthlem8  26568  logcnlem5  26777  efopn  26789  cxpmul2z  26822  cxpcn3lem  26878  cxpeq  26888  xrlimcnp  27099  cxplim  27102  o1cxp  27105  cxploglim  27108  scvxcvx  27116  jensen  27119  ftalem1  27203  ftalem2  27204  fta  27210  basellem3  27213  isppw2  27245  ppinprm  27282  chtnprm  27284  mpodvdsmulf1o  27324  dvdsmulf1o  27326  chtublem  27341  perfectlem2  27360  dchrfi  27385  dchrptlem1  27394  dchrptlem2  27395  dchrptlem3  27396  dchrsum2  27398  bposlem1  27414  bposlem3  27416  2sqlem5  27552  2sqlem6  27553  2sqlem8  27556  2sqlem10  27558  2sqb  27562  chebbnd1lem1  27599  chtppilimlem2  27604  dchrisum0flb  27640  dchrisum0fno1  27641  dchrisum0  27650  pntrsumbnd2  27697  pntpbnd1  27716  pntpbnd2  27717  pntlemp  27740  pnt3  27742  qabvle  27755  ostth2lem2  27764  ostth3  27768  ostth  27769  nolt02o  27825  nogt01o  27826  nosupprefixmo  27830  noinfprefixmo  27831  nosupbnd1lem3  27840  nosupbnd1lem4  27841  nosupbnd1lem5  27842  noinfbnd1lem3  27855  noinfbnd1lem4  27856  noinfbnd1lem5  27857  noetasuplem4  27866  noetainflem4  27870  etaslts  27952  cuteq1  27976  madebdaylemlrcut  28058  cutlt  28091  mulsuniflem  28308  bdayons  28435  addonbday  28438  om2noseqlt  28458  n0fincut  28514  bdaypw2n0bndlem  28622  bdayfinbndlem1  28626  z12sge0  28642  readdscl  28658  remulscl  28661  colinearalglem4  29200  axcontlem10  29264  upgrex  29383  smcnlem  30990  ubthlem1  31163  ubthlem3  31165  htthlem  31210  5oalem6  31952  leopmuli  32426  pjnormssi  32461  pjclem4  32492  pj3si  32500  hatomistici  32655  sumdmdlem  32711  wrdt2ind  33214  xrge0tsmsd  33334  isarchiofld  33460  ordtrest2NEWlem  34257  qqhf  34321  eulerpartlemb  34703  ballotlemfc0  34828  ballotlemfcc  34829  subfacp1lem5  35609  erdszelem7  35622  erdszelem11  35626  pconnconn  35656  txpconn  35657  connpconn  35660  sconnpi1  35664  txsconn  35666  cvxsconn  35668  cvmopnlem  35703  cvmfolem  35704  cvmliftmolem2  35707  cvmliftlem7  35716  cvmliftlem10  35719  cvmlift2lem10  35737  cvmlift3lem4  35747  cvmlift3lem8  35751  satfun  35836  msubff1  35981  wzel  36247  wsuclem  36248  btwnouttr2  36447  cgrxfr  36480  btwnxfr  36481  brcolinear  36484  lineext  36501  btwnconn1lem13  36524  midofsegid  36529  segcon2  36530  brsegle  36533  seglecgr12im  36535  segletr  36539  colinbtwnle  36543  broutsideof2  36547  btwnoutside  36550  broutsideof3  36551  outsideoftr  36554  outsideofeq  36555  outsideofeu  36556  outsidele  36557  lineunray  36572  lineelsb2  36573  linethru  36578  finminlem  36752  nn0prpwlem  36756  neibastop2lem  36794  neibastop2  36795  neibastop3  36796  topjoin  36799  tailfb  36811  axtcond  36912  relowlssretop  37931  fvineqsneq  37980  wl-sbcom2d-lem1  38136  finixpnum  38178  poimirlem6  38199  poimirlem7  38200  poimirlem13  38206  poimirlem26  38219  poimirlem29  38222  heicant  38228  opnmbllem0  38229  mblfinlem3  38232  ismblfin  38234  ovoliunnfl  38235  voliunnfl  38237  volsupnfl  38238  itg2addnclem  38244  itg2addnclem3  38246  ftc1cnnc  38265  sdclem2  38315  fdc  38318  istotbnd3  38344  isbnd2  38356  isbnd3  38357  prdsbnd  38366  cntotbnd  38369  heibor1lem  38382  heibor1  38383  heiborlem10  38393  rrncmslem  38405  ghomco  38464  1idl  38599  unichnidl  38604  disjlem18  39476  prtlem10  39563  prtlem18  39575  atlatmstc  40017  cvrexchlem  40117  paddasslem14  40531  pexmidlem5N  40672  cdleme29ex  41072  cdlemefr29exN  41100  cdleme32fva  41135  diarnN  41827  dihlsscpre  41932  isnacs3  43367  fnwe2lem2  43704  kelac1  43716  hbtlem5  43781  hbt  43783  dgraa0p  43802  ofoafg  44007  ofoafo  44009  naddcnffo  44017  fzunt  44107  fzuntd  44108  monoordxrv  46121  rlimdmafv  47837  rlimdmafv2  47918  fmtnoprmfac2  48242  perfectALTVlem2  48410  mogoldbb  48473  lindslinindsimp2  49162