Theorem expr 459

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 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 409	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  animpimp2impd  842  3expia  1117  reximddv  3275  rexlimdvaa  3285  disjxiun  5055  wereu2  5546  ordtr3  6230  fcof1  7037  knatar  7104  riota5f  7136  ovmpodf  7300  extmptsuppeq  7848  suppss  7854  suppss2  7858  wfrlem17  7965  smoord  7996  tfrlem9a  8016  oaass  8181  oelimcl  8220  oaabs2  8266  swoso  8316  eceqoveq  8396  domdifsn  8594  domunsncan  8611  omxpenlem  8612  enfixsn  8620  mapdom2  8682  frfi  8757  fofinf1o  8793  finsschain  8825  elfiun  8888  marypha1lem  8891  eqsupd  8915  eqinfd  8943  ordiso2  8973  ordtypelem6  8981  ordtypelem7  8982  ordtypelem10  8985  oismo  8998  wemapsolem  9008  brwdom2  9031  wdomtr  9033  unwdomg  9042  xpwdomg  9043  unxpwdom2  9046  cantnfval2  9126  cantnfle  9128  cantnflem1  9146  cantnf  9150  r1ordg  9201  tcrank  9307  carddomi2  9393  harval2  9420  infxpenlem  9433  infxpenc2lem2  9440  fseqenlem1  9444  dfac8clem  9452  acndom2  9474  infpwfien  9482  iunfictbso  9534  dfac12lem3  9565  infxp  9631  coflim  9677  cofsmo  9685  coftr  9689  sornom  9693  infpssrlem4  9722  enfin2i  9737  fin23lem26  9741  fin23lem27  9744  fin23lem36  9764  fin23lem40  9767  isf32lem5  9773  isf34lem4  9793  isfin1-3  9802  fin1a2lem10  9825  fin1a2lem13  9828  fin1a2s  9830  hsmexlem4  9845  ttukeylem5  9929  ttukeylem6  9930  ttukeylem7  9931  alephval2  9988  gchor  10043  fpwwe2lem7  10052  fpwwe2lem12  10057  fpwwe2  10059  pwfseqlem4a  10077  pwfseqlem4  10078  winalim2  10112  gchina  10115  inar1  10191  nqereq  10351  prlem934  10449  prlem936  10463  addsrmo  10489  mulsrmo  10490  supsrlem  10527  axpre-sup  10585  dedekind  10797  dedekindle  10798  mulge0b  11504  supaddc  11602  supmul1  11604  un0addcl  11924  un0mulcl  11925  uzwo3  12337  qbtwnre  12586  xlemul1a  12675  seqcl2  13382  seqfveq2  13386  seqshft2  13390  monoord  13394  seqsplit  13397  seqf1olem1  13403  seqid2  13410  seqhomo  13411  expnegz  13457  expcan  13527  ltexp2  13528  discr  13595  bcval5  13672  hashbc  13805  hashf1lem2  13808  seqcoll  13816  seqcoll2  13817  wrdind  14078  wrd2ind  14079  cau3lem  14708  ello1d  14874  lo1bdd2  14875  rlimclim  14897  climrlim2  14898  rlimdm  14902  rlimcn1  14939  reccn2  14947  rlimsqzlem  14999  lo1le  15002  caucvgrlem  15023  caurcvg2  15028  summolem2  15067  zsum  15069  fsum  15071  fsumf1o  15074  sumss  15075  fsumss  15076  fsumcl2lem  15082  fsumadd  15090  fsumcom2  15123  fsum0diag2  15132  fsummulc2  15133  fsumconst  15139  fsumrelem  15156  fsumrlim  15160  fsumo1  15161  divrcnv  15201  geomulcvg  15226  mertenslem2  15235  prodmolem2  15283  zprod  15285  fprod  15289  fprodf1o  15294  prodss  15295  fprodss  15296  fprodcl2lem  15298  fprodmul  15308  fproddiv  15309  fprodconst  15326  fprodn0  15327  fprodcom2  15332  ruclem8  15584  dvds0lem  15614  dvdsnegb  15621  dvdssub2  15645  bitsf1  15789  bitsshft  15818  bezoutlem3  15883  bezoutlem4  15884  isprm5  16045  isprm6  16052  hashgcdeq  16120  modprminv  16130  modprminveq  16131  reumodprminv  16135  pcqmul  16184  pcqcl  16187  pcxcl  16191  pc2dvds  16209  pcadd  16219  pcmpt  16222  pockthg  16236  infpnlem1  16240  prmreclem5  16250  vdwlem2  16312  vdwlem9  16319  vdwlem10  16320  vdwlem12  16322  ramub  16343  0ram  16350  ramub1lem2  16357  ramub1  16358  ramcl  16359  mreexexd  16913  acsfn2  16928  iscatd  16938  catpropd  16973  setcmon  17341  pleval2i  17568  psss  17818  mgmidsssn0  17876  mhmeql  17984  frmdss2  18022  frmdup3  18026  grprcan  18131  dfgrp3lem  18191  mulgnn0ass  18257  isnsg3  18306  ghmpreima  18374  ghmeql  18375  gaorber  18432  f1omvdco2  18570  psgnunilem1  18615  psgnunilem2  18617  oddvds  18669  gexdvds  18703  sylow1lem1  18717  odcau  18723  pgpssslw  18733  sylow2alem2  18737  sylow2blem3  18741  fislw  18744  lsmmod  18795  efgredlem  18867  frgpup3  18898  gsumval3  19021  gsumzres  19023  gsumzcl2  19024  gsumzf1o  19026  gsumzaddlem  19035  gsumconst  19048  gsumzmhm  19051  gsumzoppg  19058  gsum2d2lem  19087  ablfac1eulem  19188  pgpfac1lem5  19195  ablfaclem3  19203  issubdrg  19554  lss1d  19729  lmhmeql  19821  lspextmo  19822  lspsnat  19911  lsppratlem6  19918  islbs3  19921  lbsextlem4  19927  lidl1el  19985  rnasclassa  20118  mvrf1  20199  mplsubglem  20208  mpllsslem  20209  mplcoe1  20240  mplcoe5  20243  gsummoncoe1  20466  cnsubrg  20599  gsumfsum  20606  prmirredlem  20634  znidomb  20702  frgpcyg  20714  cssmre  20831  dsmmsubg  20881  dsmmlss  20882  frlmsslsp  20934  lindff1  20958  lindfrn  20959  mat1dimcrng  21080  mdetdiaglem  21201  mdetunilem7  21221  mdetunilem8  21222  mdetunilem9  21223  cpmatacl  21318  cpmatmcllem  21320  mp2pm2mplem4  21411  en2top  21587  toponmre  21695  topssnei  21726  innei  21727  clslp  21750  restcls  21783  restntr  21784  ordtrest2lem  21805  cnpco  21869  cncls2  21875  cncnpi  21880  cncnp  21882  cnconst2  21885  cnpdis  21895  lmcnp  21906  cnhaus  21956  isreg2  21979  cncmp  21994  tgcmp  22003  sscmp  22007  cmpfi  22010  cnconn  22024  iunconnlem  22029  clsconn  22032  1stcfb  22047  1stcrest  22055  2ndcctbss  22057  2ndcdisj  22058  1stcelcls  22063  1stccnp  22064  restnlly  22084  cldllycmp  22097  lly1stc  22098  dislly  22099  locfincmp  22128  comppfsc  22134  kgentopon  22140  kgenidm  22149  1stckgenlem  22155  kgencn3  22160  ptpjpre1  22173  ptbasin  22179  txcls  22206  tx2cn  22212  ptpjcn  22213  ptclsg  22217  ptcnp  22224  txdis  22234  txlly  22238  txnlly  22239  pthaus  22240  txtube  22242  txcmplem1  22243  txcmplem2  22244  txcmp  22245  txhaus  22249  txkgen  22254  xkohaus  22255  xkococnlem  22261  xkococn  22262  txconn  22291  qtopeu  22318  qtoprest  22319  regr1lem2  22342  kqreglem1  22343  cmphaushmeo  22402  xkocnv  22416  fgabs  22481  filuni  22487  trufil  22512  ufileu  22521  filufint  22522  fin1aufil  22534  elfm2  22550  rnelfmlem  22554  fmfnfmlem2  22557  fmfnfmlem4  22559  fmufil  22561  flimopn  22577  fbflim2  22579  hausflimi  22582  hausflim  22583  flimcf  22584  flimclslem  22586  flimsncls  22588  hauspwpwf1  22589  cnpflfi  22601  fclsnei  22621  fclscf  22627  flimfnfcls  22630  fclscmp  22632  ufilcmp  22634  fcfnei  22637  cnpfcf  22643  alexsublem  22646  alexsub  22647  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALTlem4  22652  ptcmplem3  22656  ptcmplem4  22657  ptcmplem5  22658  symgtgp  22708  tgpconncompeqg  22714  tgpconncomp  22715  ghmcnp  22717  tgpt0  22721  qustgplem  22723  haustsms2  22739  tsmsgsum  22741  tsmsres  22746  tsmsxp  22757  imasdsf1olem  22977  xbln0  23018  blssps  23028  blss  23029  neibl  23105  blcld  23109  metss  23112  metequiv2  23114  met1stc  23125  metrest  23128  prdsxmslem2  23133  metcnp3  23144  nrmmetd  23178  nlmvscnlem1  23289  nrginvrcnlem  23294  nmoleub  23334  icccmplem2  23425  icccmp  23427  reconnlem2  23429  xrge0tsms  23436  metdstri  23453  metdseq0  23456  metdscn  23458  cnmpopc  23526  lebnumlem3  23561  pcoval2  23614  pcopt  23620  nmoleub2lem  23712  nmhmcn  23718  ipcnlem1  23842  cfilfcls  23871  cmetcaulem  23885  iscmet3lem2  23889  iscmet3  23890  equivcau  23897  caubl  23905  bcthlem2  23922  bcthlem3  23923  bcthlem4  23924  bcthlem5  23925  ivthlem2  24047  ivthlem3  24048  ovoliunlem2  24098  ovolicc2lem2  24113  ovolicc2lem5  24116  ovolicc2  24117  ismbl2  24122  nulmbl  24130  nulmbl2  24131  unmbl  24132  shftmbl  24133  voliunlem3  24147  volsup  24151  ioombl1lem4  24156  ioombl1  24157  icombl  24159  ioombl  24160  uniioombl  24184  opnmbllem  24196  volivth  24202  vitali  24208  mbflimsup  24261  i1fadd  24290  itg1addlem4  24294  itg2le  24334  itg2seq  24337  itg2lea  24339  itg2splitlem  24343  itg2split  24344  itg2mono  24348  itg2gt0  24355  itg2cnlem2  24357  itgss  24406  itgfsum  24421  itgcn  24437  ellimc3  24471  limcco  24485  limciun  24486  dvnres  24522  dvnfre  24543  rolle  24581  c1liplem1  24587  dvivth  24601  dvne0  24602  lhop1lem  24604  lhop1  24605  lhop  24607  dvcnvrelem1  24608  dvfsumrlim  24622  dvfsum2  24625  ftc1a  24628  ftc1lem6  24632  itgsubst  24640  tdeglem4  24648  mdegaddle  24662  mdegvscale  24663  mdegmullem  24666  deg1tmle  24705  ply1divex  24724  dvdsq1p  24748  fta1g  24755  fta1b  24757  plyco0  24776  coeeulem  24808  dgrlem  24813  plyco  24825  coemullem  24834  dgreq0  24849  dgrco  24859  plydivex  24880  quotcan  24892  aannenlem1  24911  aalioulem2  24916  aalioulem3  24917  taylthlem1  24955  ulmbdd  24980  itgulm  24990  radcnvlt1  25000  psercnlem1  25007  abelthlem2  25014  abelthlem8  25021  logcnlem5  25223  efopn  25235  cxpmul2z  25268  cxpcn3lem  25322  cxpeq  25332  xrlimcnp  25540  cxplim  25543  o1cxp  25546  cxploglim  25549  scvxcvx  25557  jensen  25560  ftalem1  25644  ftalem2  25645  fta  25651  basellem3  25654  isppw2  25686  ppinprm  25723  chtnprm  25725  dvdsmulf1o  25765  chtublem  25781  perfectlem2  25800  dchrfi  25825  dchrptlem1  25834  dchrptlem2  25835  dchrptlem3  25836  dchrsum2  25838  bposlem1  25854  bposlem3  25856  2sqlem5  25992  2sqlem6  25993  2sqlem8  25996  2sqlem10  25998  2sqb  26002  chebbnd1lem1  26039  chtppilimlem2  26044  dchrisum0flb  26080  dchrisum0fno1  26081  dchrisum0  26090  pntrsumbnd2  26137  pntpbnd1  26156  pntpbnd2  26157  pntlemp  26180  pnt3  26182  qabvle  26195  ostth2lem2  26204  ostth3  26208  ostth  26209  colinearalglem4  26689  axcontlem10  26753  upgrex  26871  smcnlem  28468  ubthlem1  28641  ubthlem3  28643  htthlem  28688  5oalem6  29430  leopmuli  29904  pjnormssi  29939  pjclem4  29970  pj3si  29978  hatomistici  30133  sumdmdlem  30189  wrdt2ind  30622  xrge0tsmsd  30687  isarchiofld  30885  ordtrest2NEWlem  31160  qqhf  31222  eulerpartlemb  31621  ballotlemfc0  31745  ballotlemfcc  31746  sgn3da  31794  subfacp1lem5  32426  erdszelem7  32439  erdszelem11  32443  pconnconn  32473  txpconn  32474  connpconn  32477  sconnpi1  32481  txsconn  32483  cvxsconn  32485  cvmopnlem  32520  cvmfolem  32521  cvmliftmolem2  32524  cvmliftlem7  32533  cvmliftlem10  32536  cvmlift2lem10  32554  cvmlift3lem4  32564  cvmlift3lem8  32568  satfun  32653  msubff1  32798  frpomin  33073  wzel  33106  wsuclem  33107  frrlem14  33131  nolt02o  33194  nosupbnd1lem3  33205  nosupbnd1lem4  33206  nosupbnd1lem5  33207  noetalem3  33214  btwnouttr2  33478  cgrxfr  33511  btwnxfr  33512  brcolinear  33515  lineext  33532  btwnconn1lem13  33555  midofsegid  33560  segcon2  33561  brsegle  33564  seglecgr12im  33566  segletr  33570  colinbtwnle  33574  broutsideof2  33578  btwnoutside  33581  broutsideof3  33582  outsideoftr  33585  outsideofeq  33586  outsideofeu  33587  outsidele  33588  lineunray  33603  lineelsb2  33604  linethru  33609  finminlem  33661  nn0prpwlem  33665  neibastop2lem  33703  neibastop2  33704  neibastop3  33705  topjoin  33708  tailfb  33720  relowlssretop  34638  fvineqsneq  34687  wl-sbcom2d-lem1  34789  finixpnum  34871  poimirlem6  34892  poimirlem7  34893  poimirlem13  34899  poimirlem26  34912  poimirlem29  34915  heicant  34921  opnmbllem0  34922  mblfinlem3  34925  ismblfin  34927  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  itg2addnclem  34937  itg2addnclem3  34939  ftc1cnnc  34960  sdclem2  35011  fdc  35014  istotbnd3  35043  isbnd2  35055  isbnd3  35056  prdsbnd  35065  cntotbnd  35068  heibor1lem  35081  heibor1  35082  heiborlem10  35092  rrncmslem  35104  ghomco  35163  1idl  35298  unichnidl  35303  prtlem10  35995  prtlem18  36007  atlatmstc  36449  cvrexchlem  36549  paddasslem14  36963  pexmidlem5N  37104  cdleme29ex  37504  cdlemefr29exN  37532  cdleme32fva  37567  diarnN  38259  dihlsscpre  38364  isnacs3  39300  fnwe2lem2  39644  kelac1  39656  hbtlem5  39721  hbt  39723  dgraa0p  39742  monoordxrv  41751  rlimdmafv  43370  rlimdmafv2  43451  fmtnoprmfac2  43723  perfectALTVlem2  43881  mogoldbb  43944  mgmhmeql  44064  lindslinindsimp2  44512