Theorem expr 460

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 424	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 410	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:  animpimp2impd  843  3expia  1118  reximddv  3199  rexlimdvaa  3209  disjxiun  5032  wereu2  5524  ordtr3  6218  fcof1  7040  knatar  7109  riota5f  7141  ovmpodf  7306  extmptsuppeq  7867  suppss  7873  suppssOLD  7874  suppss2  7879  wfrlem17  7986  smoord  8017  tfrlem9a  8037  oaass  8202  oelimcl  8241  oaabs2  8287  swoso  8337  eceqoveq  8417  domdifsn  8626  domunsncan  8643  omxpenlem  8644  enfixsn  8652  mapdom2  8715  frfi  8801  fofinf1o  8837  finsschain  8869  elfiun  8932  marypha1lem  8935  eqsupd  8959  eqinfd  8987  ordiso2  9017  ordtypelem6  9025  ordtypelem7  9026  ordtypelem10  9029  oismo  9042  wemapsolem  9052  brwdom2  9075  wdomtr  9077  unwdomg  9086  xpwdomg  9087  unxpwdom2  9090  cantnfval2  9170  cantnfle  9172  cantnflem1  9190  cantnf  9194  r1ordg  9245  tcrank  9351  carddomi2  9437  harval2  9464  infxpenlem  9478  infxpenc2lem2  9485  fseqenlem1  9489  dfac8clem  9497  acndom2  9519  infpwfien  9527  iunfictbso  9579  dfac12lem3  9610  infxp  9680  coflim  9726  cofsmo  9734  coftr  9738  sornom  9742  infpssrlem4  9771  enfin2i  9786  fin23lem26  9790  fin23lem27  9793  fin23lem36  9813  fin23lem40  9816  isf32lem5  9822  isf34lem4  9842  isfin1-3  9851  fin1a2lem10  9874  fin1a2lem13  9877  fin1a2s  9879  hsmexlem4  9894  ttukeylem5  9978  ttukeylem6  9979  ttukeylem7  9980  alephval2  10037  gchor  10092  fpwwe2lem6  10101  fpwwe2lem11  10106  fpwwe2  10108  pwfseqlem4a  10126  pwfseqlem4  10127  winalim2  10161  gchina  10164  inar1  10240  nqereq  10400  prlem934  10498  prlem936  10512  addsrmo  10538  mulsrmo  10539  supsrlem  10576  axpre-sup  10634  dedekind  10846  dedekindle  10847  mulge0b  11553  supaddc  11649  supmul1  11651  un0addcl  11972  un0mulcl  11973  uzwo3  12388  qbtwnre  12638  xlemul1a  12727  seqcl2  13443  seqfveq2  13447  seqshft2  13451  monoord  13455  seqsplit  13458  seqf1olem1  13464  seqid2  13471  seqhomo  13472  expnegz  13518  expcan  13588  ltexp2  13589  discr  13656  bcval5  13733  hashbc  13866  hashf1lem2  13871  seqcoll  13879  seqcoll2  13880  wrdind  14136  wrd2ind  14137  cau3lem  14767  ello1d  14933  lo1bdd2  14934  rlimclim  14956  climrlim2  14957  rlimdm  14961  rlimcn1  14998  reccn2  15006  rlimsqzlem  15058  lo1le  15061  caucvgrlem  15082  caurcvg2  15087  summolem2  15126  zsum  15128  fsum  15130  fsumf1o  15133  sumss  15134  fsumss  15135  fsumcl2lem  15141  fsumadd  15149  fsumcom2  15182  fsum0diag2  15191  fsummulc2  15192  fsumconst  15198  fsumrelem  15215  fsumrlim  15219  fsumo1  15220  divrcnv  15260  geomulcvg  15285  mertenslem2  15294  prodmolem2  15342  zprod  15344  fprod  15348  fprodf1o  15353  prodss  15354  fprodss  15355  fprodcl2lem  15357  fprodmul  15367  fproddiv  15368  fprodconst  15385  fprodn0  15386  fprodcom2  15391  ruclem8  15643  dvds0lem  15673  dvdsnegb  15680  dvdssub2  15707  bitsf1  15850  bitsshft  15879  bezoutlem3  15945  bezoutlem4  15946  isprm5  16108  isprm6  16115  hashgcdeq  16186  modprminv  16196  modprminveq  16197  reumodprminv  16201  pcqmul  16250  pcqcl  16253  pcxcl  16257  pc2dvds  16275  pcadd  16285  pcmpt  16288  pockthg  16302  infpnlem1  16306  prmreclem5  16316  vdwlem2  16378  vdwlem9  16385  vdwlem10  16386  vdwlem12  16388  ramub  16409  0ram  16416  ramub1lem2  16423  ramub1  16424  ramcl  16425  mreexexd  16982  acsfn2  16997  iscatd  17007  catpropd  17042  setcmon  17418  pleval2i  17645  psss  17895  mgmidsssn0  17953  mhmeql  18061  frmdss2  18099  frmdup3  18103  grprcan  18209  dfgrp3lem  18269  mulgnn0ass  18335  isnsg3  18384  ghmpreima  18452  ghmeql  18453  gaorber  18510  f1omvdco2  18648  psgnunilem1  18693  psgnunilem2  18695  oddvds  18747  gexdvds  18781  sylow1lem1  18795  odcau  18801  pgpssslw  18811  sylow2alem2  18815  sylow2blem3  18819  fislw  18822  lsmmod  18873  efgredlem  18945  frgpup3  18976  gsumval3  19100  gsumzres  19102  gsumzcl2  19103  gsumzf1o  19105  gsumzaddlem  19114  gsumconst  19127  gsumzmhm  19130  gsumzoppg  19137  gsum2d2lem  19166  ablfac1eulem  19267  pgpfac1lem5  19274  ablfaclem3  19282  issubdrg  19633  lss1d  19808  lmhmeql  19900  lspextmo  19901  lspsnat  19990  lsppratlem6  19997  islbs3  20000  lbsextlem4  20006  lidl1el  20064  cnsubrg  20231  gsumfsum  20238  prmirredlem  20267  znidomb  20334  frgpcyg  20346  cssmre  20463  dsmmsubg  20513  dsmmlss  20514  frlmsslsp  20566  lindff1  20590  lindfrn  20591  rnasclassa  20663  mvrf1  20758  mplsubglem  20769  mpllsslem  20770  mplcoe1  20802  mplcoe5  20805  gsummoncoe1  21033  mat1dimcrng  21182  mdetdiaglem  21303  mdetunilem7  21323  mdetunilem8  21324  mdetunilem9  21325  cpmatacl  21421  cpmatmcllem  21423  mp2pm2mplem4  21514  en2top  21690  toponmre  21798  topssnei  21829  innei  21830  clslp  21853  restcls  21886  restntr  21887  ordtrest2lem  21908  cnpco  21972  cncls2  21978  cncnpi  21983  cncnp  21985  cnconst2  21988  cnpdis  21998  lmcnp  22009  cnhaus  22059  isreg2  22082  cncmp  22097  tgcmp  22106  sscmp  22110  cmpfi  22113  cnconn  22127  iunconnlem  22132  clsconn  22135  1stcfb  22150  1stcrest  22158  2ndcctbss  22160  2ndcdisj  22161  1stcelcls  22166  1stccnp  22167  restnlly  22187  cldllycmp  22200  lly1stc  22201  dislly  22202  locfincmp  22231  comppfsc  22237  kgentopon  22243  kgenidm  22252  1stckgenlem  22258  kgencn3  22263  ptpjpre1  22276  ptbasin  22282  txcls  22309  tx2cn  22315  ptpjcn  22316  ptclsg  22320  ptcnp  22327  txdis  22337  txlly  22341  txnlly  22342  pthaus  22343  txtube  22345  txcmplem1  22346  txcmplem2  22347  txcmp  22348  txhaus  22352  txkgen  22357  xkohaus  22358  xkococnlem  22364  xkococn  22365  txconn  22394  qtopeu  22421  qtoprest  22422  regr1lem2  22445  kqreglem1  22446  cmphaushmeo  22505  xkocnv  22519  fgabs  22584  filuni  22590  trufil  22615  ufileu  22624  filufint  22625  fin1aufil  22637  elfm2  22653  rnelfmlem  22657  fmfnfmlem2  22660  fmfnfmlem4  22662  fmufil  22664  flimopn  22680  fbflim2  22682  hausflimi  22685  hausflim  22686  flimcf  22687  flimclslem  22689  flimsncls  22691  hauspwpwf1  22692  cnpflfi  22704  fclsnei  22724  fclscf  22730  flimfnfcls  22733  fclscmp  22735  ufilcmp  22737  fcfnei  22740  cnpfcf  22746  alexsublem  22749  alexsub  22750  alexsubALTlem2  22753  alexsubALTlem3  22754  alexsubALTlem4  22755  ptcmplem3  22759  ptcmplem4  22760  ptcmplem5  22761  symgtgp  22811  tgpconncompeqg  22817  tgpconncomp  22818  ghmcnp  22820  tgpt0  22824  qustgplem  22826  haustsms2  22842  tsmsgsum  22844  tsmsres  22849  tsmsxp  22860  imasdsf1olem  23080  xbln0  23121  blssps  23131  blss  23132  neibl  23208  blcld  23212  metss  23215  metequiv2  23217  met1stc  23228  metrest  23231  prdsxmslem2  23236  metcnp3  23247  nrmmetd  23281  nlmvscnlem1  23393  nrginvrcnlem  23398  nmoleub  23438  icccmplem2  23529  icccmp  23531  reconnlem2  23533  xrge0tsms  23540  metdstri  23557  metdseq0  23560  metdscn  23562  cnmpopc  23634  lebnumlem3  23669  pcoval2  23722  pcopt  23728  nmoleub2lem  23820  nmhmcn  23826  ipcnlem1  23950  cfilfcls  23979  cmetcaulem  23993  iscmet3lem2  23997  iscmet3  23998  equivcau  24005  caubl  24013  bcthlem2  24030  bcthlem3  24031  bcthlem4  24032  bcthlem5  24033  ivthlem2  24157  ivthlem3  24158  ovoliunlem2  24208  ovolicc2lem2  24223  ovolicc2lem5  24226  ovolicc2  24227  ismbl2  24232  nulmbl  24240  nulmbl2  24241  unmbl  24242  shftmbl  24243  voliunlem3  24257  volsup  24261  ioombl1lem4  24266  ioombl1  24267  icombl  24269  ioombl  24270  uniioombl  24294  opnmbllem  24306  volivth  24312  vitali  24318  mbflimsup  24371  i1fadd  24400  itg1addlem4  24404  itg2le  24444  itg2seq  24447  itg2lea  24449  itg2splitlem  24453  itg2split  24454  itg2mono  24458  itg2gt0  24465  itg2cnlem2  24467  itgss  24516  itgfsum  24531  itgcn  24549  ellimc3  24583  limcco  24597  limciun  24598  dvnres  24635  dvnfre  24656  rolle  24694  c1liplem1  24700  dvivth  24714  dvne0  24715  lhop1lem  24717  lhop1  24718  lhop  24720  dvcnvrelem1  24721  dvfsumrlim  24735  dvfsum2  24738  ftc1a  24741  ftc1lem6  24745  itgsubst  24753  tdeglem4  24764  tdeglem4OLD  24765  mdegaddle  24779  mdegvscale  24780  mdegmullem  24783  deg1tmle  24822  ply1divex  24841  dvdsq1p  24865  fta1g  24872  fta1b  24874  plyco0  24893  coeeulem  24925  dgrlem  24930  plyco  24942  coemullem  24951  dgreq0  24966  dgrco  24976  plydivex  24997  quotcan  25009  aannenlem1  25028  aalioulem2  25033  aalioulem3  25034  taylthlem1  25072  ulmbdd  25097  itgulm  25107  radcnvlt1  25117  psercnlem1  25124  abelthlem2  25131  abelthlem8  25138  logcnlem5  25341  efopn  25353  cxpmul2z  25386  cxpcn3lem  25440  cxpeq  25450  xrlimcnp  25658  cxplim  25661  o1cxp  25664  cxploglim  25667  scvxcvx  25675  jensen  25678  ftalem1  25762  ftalem2  25763  fta  25769  basellem3  25772  isppw2  25804  ppinprm  25841  chtnprm  25843  dvdsmulf1o  25883  chtublem  25899  perfectlem2  25918  dchrfi  25943  dchrptlem1  25952  dchrptlem2  25953  dchrptlem3  25954  dchrsum2  25956  bposlem1  25972  bposlem3  25974  2sqlem5  26110  2sqlem6  26111  2sqlem8  26114  2sqlem10  26116  2sqb  26120  chebbnd1lem1  26157  chtppilimlem2  26162  dchrisum0flb  26198  dchrisum0fno1  26199  dchrisum0  26208  pntrsumbnd2  26255  pntpbnd1  26274  pntpbnd2  26275  pntlemp  26298  pnt3  26300  qabvle  26313  ostth2lem2  26322  ostth3  26326  ostth  26327  colinearalglem4  26807  axcontlem10  26871  upgrex  26989  smcnlem  28584  ubthlem1  28757  ubthlem3  28759  htthlem  28804  5oalem6  29546  leopmuli  30020  pjnormssi  30055  pjclem4  30086  pj3si  30094  hatomistici  30249  sumdmdlem  30305  wrdt2ind  30753  xrge0tsmsd  30847  isarchiofld  31046  ordtrest2NEWlem  31397  qqhf  31459  eulerpartlemb  31858  ballotlemfc0  31982  ballotlemfcc  31983  sgn3da  32031  subfacp1lem5  32666  erdszelem7  32679  erdszelem11  32683  pconnconn  32713  txpconn  32714  connpconn  32717  sconnpi1  32721  txsconn  32723  cvxsconn  32725  cvmopnlem  32760  cvmfolem  32761  cvmliftmolem2  32764  cvmliftlem7  32773  cvmliftlem10  32776  cvmlift2lem10  32794  cvmlift3lem4  32804  cvmlift3lem8  32808  satfun  32893  msubff1  33038  frpomin  33329  wzel  33377  wsuclem  33378  frrlem14  33402  naddssim  33426  nolt02o  33487  nogt01o  33488  nosupprefixmo  33492  noinfprefixmo  33493  nosupbnd1lem3  33502  nosupbnd1lem4  33503  nosupbnd1lem5  33504  noinfbnd1lem3  33517  noinfbnd1lem4  33518  noinfbnd1lem5  33519  noetasuplem4  33528  noetainflem4  33532  etasslt  33594  oldlim  33652  madebdayim  33653  madebdaylemlrcut  33662  btwnouttr2  33899  cgrxfr  33932  btwnxfr  33933  brcolinear  33936  lineext  33953  btwnconn1lem13  33976  midofsegid  33981  segcon2  33982  brsegle  33985  seglecgr12im  33987  segletr  33991  colinbtwnle  33995  broutsideof2  33999  btwnoutside  34002  broutsideof3  34003  outsideoftr  34006  outsideofeq  34007  outsideofeu  34008  outsidele  34009  lineunray  34024  lineelsb2  34025  linethru  34030  finminlem  34082  nn0prpwlem  34086  neibastop2lem  34124  neibastop2  34125  neibastop3  34126  topjoin  34129  tailfb  34141  relowlssretop  35086  fvineqsneq  35135  wl-sbcom2d-lem1  35266  finixpnum  35348  poimirlem6  35369  poimirlem7  35370  poimirlem13  35376  poimirlem26  35389  poimirlem29  35392  heicant  35398  opnmbllem0  35399  mblfinlem3  35402  ismblfin  35404  ovoliunnfl  35405  voliunnfl  35407  volsupnfl  35408  itg2addnclem  35414  itg2addnclem3  35416  ftc1cnnc  35435  sdclem2  35486  fdc  35489  istotbnd3  35515  isbnd2  35527  isbnd3  35528  prdsbnd  35537  cntotbnd  35540  heibor1lem  35553  heibor1  35554  heiborlem10  35564  rrncmslem  35576  ghomco  35635  1idl  35770  unichnidl  35775  prtlem10  36467  prtlem18  36479  atlatmstc  36921  cvrexchlem  37021  paddasslem14  37435  pexmidlem5N  37576  cdleme29ex  37976  cdlemefr29exN  38004  cdleme32fva  38039  diarnN  38731  dihlsscpre  38836  isnacs3  40052  fnwe2lem2  40396  kelac1  40408  hbtlem5  40473  hbt  40475  dgraa0p  40494  monoordxrv  42515  rlimdmafv  44129  rlimdmafv2  44210  fmtnoprmfac2  44480  perfectALTVlem2  44635  mogoldbb  44698  mgmhmeql  44818  lindslinindsimp2  45265