Theorem expr 456

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 406	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 207  df-an 396

This theorem is referenced by:  animpimp2impd  846  3expia  1121  rexlimdvaa  3155  reximddv  3170  disjxiun  5146  wereu2  5687  frpomin  6366  ordtr3  6434  fcof1  7311  knatar  7381  riota5f  7420  ovmpodf  7593  extmptsuppeq  8218  suppss  8224  suppss2  8230  frrlem14  8329  fprresex  8340  wfrlem17OLD  8370  smoord  8410  tfrlem9a  8431  oaass  8604  oelimcl  8643  oaabs2  8692  cofon1  8715  naddssim  8728  swoso  8784  eceqoveq  8867  domdifsn  9099  domunsncan  9117  omxpenlem  9118  enfixsn  9126  mapdom2  9193  frfi  9325  fofinf1o  9376  finsschain  9403  elfiun  9474  marypha1lem  9477  eqsupd  9501  eqinfd  9529  ordiso2  9559  ordtypelem6  9567  ordtypelem7  9568  ordtypelem10  9571  oismo  9584  wemapsolem  9594  brwdom2  9617  wdomtr  9619  unwdomg  9628  xpwdomg  9629  unxpwdom2  9632  cantnfval2  9713  cantnfle  9715  cantnflem1  9733  cantnf  9737  r1ordg  9822  tcrank  9928  carddomi2  10014  harval2  10041  infxpenlem  10057  infxpenc2lem2  10064  fseqenlem1  10068  dfac8clem  10076  acndom2  10098  infpwfien  10106  iunfictbso  10158  dfac12lem3  10190  infxp  10258  coflim  10305  cofsmo  10313  coftr  10317  sornom  10321  infpssrlem4  10350  enfin2i  10365  fin23lem26  10369  fin23lem27  10372  fin23lem36  10392  fin23lem40  10395  isf32lem5  10401  isf34lem4  10421  isfin1-3  10430  fin1a2lem10  10453  fin1a2lem13  10456  fin1a2s  10458  hsmexlem4  10473  ttukeylem5  10557  ttukeylem6  10558  ttukeylem7  10559  alephval2  10616  gchor  10671  fpwwe2lem6  10680  fpwwe2lem11  10685  fpwwe2  10687  pwfseqlem4a  10705  pwfseqlem4  10706  winalim2  10740  gchina  10743  inar1  10819  nqereq  10979  prlem934  11077  prlem936  11091  addsrmo  11117  mulsrmo  11118  supsrlem  11155  axpre-sup  11213  dedekind  11428  dedekindle  11429  mulge0b  12142  supaddc  12239  supmul1  12241  un0addcl  12563  un0mulcl  12564  uzwo3  12989  qbtwnre  13244  xlemul1a  13333  seqcl2  14064  seqfveq2  14068  seqshft2  14072  monoord  14076  seqsplit  14079  seqf1olem1  14085  seqid2  14092  seqhomo  14093  expnegz  14140  expcan  14212  ltexp2  14213  discr  14282  bcval5  14360  hashbc  14495  hashf1lem2  14498  seqcoll  14506  seqcoll2  14507  wrdind  14763  wrd2ind  14764  cau3lem  15396  ello1d  15562  lo1bdd2  15563  rlimclim  15585  climrlim2  15586  rlimdm  15590  rlimcn1  15627  reccn2  15636  rlimsqzlem  15688  lo1le  15691  caucvgrlem  15712  caurcvg2  15717  summolem2  15755  zsum  15757  fsum  15759  fsumf1o  15762  sumss  15763  fsumss  15764  fsumcl2lem  15770  fsumadd  15779  fsumcom2  15813  fsum0diag2  15822  fsummulc2  15823  fsumconst  15829  fsumrelem  15846  fsumrlim  15850  fsumo1  15851  divrcnv  15891  geomulcvg  15915  mertenslem2  15924  prodmolem2  15974  zprod  15976  fprod  15980  fprodf1o  15985  prodss  15986  fprodss  15987  fprodcl2lem  15989  fprodmul  15999  fproddiv  16000  fprodconst  16017  fprodn0  16018  fprodcom2  16023  ruclem8  16276  dvds0lem  16307  dvdsnegb  16314  dvdssub2  16341  bitsf1  16486  bitsshft  16515  bezoutlem3  16581  bezoutlem4  16582  isprm5  16747  isprm6  16754  hashgcdeq  16829  modprminv  16839  modprminveq  16840  reumodprminv  16844  pcqmul  16893  pcqcl  16896  pcxnn0cl  16900  pcxcl  16901  pc2dvds  16919  pcadd  16929  pcmpt  16932  pockthg  16946  infpnlem1  16950  prmreclem5  16960  vdwlem2  17022  vdwlem9  17029  vdwlem10  17030  vdwlem12  17032  ramub  17053  0ram  17060  ramub1lem2  17067  ramub1  17068  ramcl  17069  mreexexd  17699  acsfn2  17714  iscatd  17724  catpropd  17760  setcmon  18147  pleval2i  18400  psss  18644  mgmidsssn0  18704  mgmhmeql  18748  mhmeql  18858  frmdss2  18895  frmdup3  18899  grprcan  19010  dfgrp3lem  19075  mulgnn0ass  19147  isnsg3  19197  ghmpreima  19275  ghmeql  19276  gaorber  19345  f1omvdco2  19487  psgnunilem1  19532  psgnunilem2  19534  oddvds  19586  gexdvds  19623  sylow1lem1  19637  odcau  19643  pgpssslw  19653  sylow2alem2  19657  sylow2blem3  19661  fislw  19664  lsmmod  19714  efgredlem  19786  frgpup3  19817  gsumval3  19946  gsumzres  19948  gsumzcl2  19949  gsumzf1o  19951  gsumzaddlem  19960  gsumconst  19973  gsumzmhm  19976  gsumzoppg  19983  gsum2d2lem  20012  ablfac1eulem  20113  pgpfac1lem5  20120  ablfaclem3  20128  issubdrg  20804  lss1d  20985  lmhmeql  21078  lspextmo  21079  lspsnat  21171  lsppratlem6  21178  islbs3  21181  lbsextlem4  21187  lidl1el  21260  cnsubrg  21469  gsumfsum  21476  prmirredlem  21507  znidomb  21604  frgpcyg  21616  cssmre  21735  dsmmsubg  21787  dsmmlss  21788  frlmsslsp  21840  lindff1  21864  lindfrn  21865  rnasclassa  21939  mvrf1  22030  mplsubglem  22043  mpllsslem  22044  mplcoe1  22079  mplcoe5  22082  gsummoncoe1  22334  mat1dimcrng  22505  mdetdiaglem  22626  mdetunilem7  22646  mdetunilem8  22647  mdetunilem9  22648  cpmatacl  22744  cpmatmcllem  22746  mp2pm2mplem4  22837  en2top  23014  toponmre  23123  topssnei  23154  innei  23155  clslp  23178  restcls  23211  restntr  23212  ordtrest2lem  23233  cnpco  23297  cncls2  23303  cncnpi  23308  cncnp  23310  cnconst2  23313  cnpdis  23323  lmcnp  23334  cnhaus  23384  isreg2  23407  cncmp  23422  tgcmp  23431  sscmp  23435  cmpfi  23438  cnconn  23452  iunconnlem  23457  clsconn  23460  1stcfb  23475  1stcrest  23483  2ndcctbss  23485  2ndcdisj  23486  1stcelcls  23491  1stccnp  23492  restnlly  23512  cldllycmp  23525  lly1stc  23526  dislly  23527  locfincmp  23556  comppfsc  23562  kgentopon  23568  kgenidm  23577  1stckgenlem  23583  kgencn3  23588  ptpjpre1  23601  ptbasin  23607  txcls  23634  tx2cn  23640  ptpjcn  23641  ptclsg  23645  ptcnp  23652  txdis  23662  txlly  23666  txnlly  23667  pthaus  23668  txtube  23670  txcmplem1  23671  txcmplem2  23672  txcmp  23673  txhaus  23677  txkgen  23682  xkohaus  23683  xkococnlem  23689  xkococn  23690  txconn  23719  qtopeu  23746  qtoprest  23747  regr1lem2  23770  kqreglem1  23771  cmphaushmeo  23830  xkocnv  23844  fgabs  23909  filuni  23915  trufil  23940  ufileu  23949  filufint  23950  fin1aufil  23962  elfm2  23978  rnelfmlem  23982  fmfnfmlem2  23985  fmfnfmlem4  23987  fmufil  23989  flimopn  24005  fbflim2  24007  hausflimi  24010  hausflim  24011  flimcf  24012  flimclslem  24014  flimsncls  24016  hauspwpwf1  24017  cnpflfi  24029  fclsnei  24049  fclscf  24055  flimfnfcls  24058  fclscmp  24060  ufilcmp  24062  fcfnei  24065  cnpfcf  24071  alexsublem  24074  alexsub  24075  alexsubALTlem2  24078  alexsubALTlem3  24079  alexsubALTlem4  24080  ptcmplem3  24084  ptcmplem4  24085  ptcmplem5  24086  symgtgp  24136  tgpconncompeqg  24142  tgpconncomp  24143  ghmcnp  24145  tgpt0  24149  qustgplem  24151  haustsms2  24167  tsmsgsum  24169  tsmsres  24174  tsmsxp  24185  imasdsf1olem  24405  xbln0  24446  blssps  24456  blss  24457  neibl  24536  blcld  24540  metss  24543  metequiv2  24545  met1stc  24556  metrest  24559  prdsxmslem2  24564  metcnp3  24575  nrmmetd  24609  nlmvscnlem1  24729  nrginvrcnlem  24734  nmoleub  24774  icccmplem2  24867  icccmp  24869  reconnlem2  24871  xrge0tsms  24878  metdstri  24895  metdseq0  24898  metdscn  24900  cnmpopc  24977  lebnumlem3  25017  pcoval2  25071  pcopt  25077  nmoleub2lem  25169  nmhmcn  25175  ipcnlem1  25301  cfilfcls  25330  cmetcaulem  25344  iscmet3lem2  25348  iscmet3  25349  equivcau  25356  caubl  25364  bcthlem2  25381  bcthlem3  25382  bcthlem4  25383  bcthlem5  25384  ivthlem2  25509  ivthlem3  25510  ovoliunlem2  25560  ovolicc2lem2  25575  ovolicc2lem5  25578  ovolicc2  25579  ismbl2  25584  nulmbl  25592  nulmbl2  25593  unmbl  25594  shftmbl  25595  voliunlem3  25609  volsup  25613  ioombl1lem4  25618  ioombl1  25619  icombl  25621  ioombl  25622  uniioombl  25646  opnmbllem  25658  volivth  25664  vitali  25670  mbflimsup  25723  i1fadd  25752  itg1addlem4  25756  itg1addlem4OLD  25757  itg2le  25797  itg2seq  25800  itg2lea  25802  itg2splitlem  25806  itg2split  25807  itg2mono  25811  itg2gt0  25818  itg2cnlem2  25820  itgss  25870  itgfsum  25885  itgcn  25903  ellimc3  25937  limcco  25951  limciun  25952  dvnres  25990  dvnfre  26013  rolle  26051  c1liplem1  26058  dvivth  26072  dvne0  26073  lhop1lem  26075  lhop1  26076  lhop  26078  dvcnvrelem1  26079  dvfsumrlim  26095  dvfsum2  26098  ftc1a  26101  ftc1lem6  26105  itgsubst  26113  tdeglem4  26122  mdegaddle  26136  mdegvscale  26137  mdegmullem  26140  deg1tmle  26180  ply1divex  26199  dvdsq1p  26225  fta1g  26232  fta1b  26234  plyco0  26254  coeeulem  26286  dgrlem  26291  plyco  26303  coemullem  26312  dgreq0  26328  dgrco  26338  plydivex  26362  quotcan  26374  aannenlem1  26393  aalioulem2  26398  aalioulem3  26399  taylthlem1  26438  ulmbdd  26464  itgulm  26474  radcnvlt1  26484  psercnlem1  26492  abelthlem2  26499  abelthlem8  26506  logcnlem5  26711  efopn  26723  cxpmul2z  26756  cxpcn3lem  26813  cxpeq  26823  xrlimcnp  27034  cxplim  27038  o1cxp  27041  cxploglim  27044  scvxcvx  27052  jensen  27055  ftalem1  27139  ftalem2  27140  fta  27146  basellem3  27149  isppw2  27181  ppinprm  27218  chtnprm  27220  mpodvdsmulf1o  27260  dvdsmulf1o  27262  chtublem  27278  perfectlem2  27297  dchrfi  27322  dchrptlem1  27331  dchrptlem2  27332  dchrptlem3  27333  dchrsum2  27335  bposlem1  27351  bposlem3  27353  2sqlem5  27489  2sqlem6  27490  2sqlem8  27493  2sqlem10  27495  2sqb  27499  chebbnd1lem1  27536  chtppilimlem2  27541  dchrisum0flb  27577  dchrisum0fno1  27578  dchrisum0  27587  pntrsumbnd2  27634  pntpbnd1  27653  pntpbnd2  27654  pntlemp  27677  pnt3  27679  qabvle  27692  ostth2lem2  27701  ostth3  27705  ostth  27706  nolt02o  27763  nogt01o  27764  nosupprefixmo  27768  noinfprefixmo  27769  nosupbnd1lem3  27778  nosupbnd1lem4  27779  nosupbnd1lem5  27780  noinfbnd1lem3  27793  noinfbnd1lem4  27794  noinfbnd1lem5  27795  noetasuplem4  27804  noetainflem4  27808  etasslt  27881  cuteq1  27901  madebdaylemlrcut  27960  cutlt  27989  mulsuniflem  28198  om2noseqlt  28328  readdscl  28454  remulscl  28457  colinearalglem4  28947  axcontlem10  29011  upgrex  29132  smcnlem  30739  ubthlem1  30912  ubthlem3  30914  htthlem  30959  5oalem6  31701  leopmuli  32175  pjnormssi  32210  pjclem4  32241  pj3si  32249  hatomistici  32404  sumdmdlem  32460  wrdt2ind  32936  xrge0tsmsd  33061  isarchiofld  33340  ordtrest2NEWlem  33896  qqhf  33962  eulerpartlemb  34363  ballotlemfc0  34487  ballotlemfcc  34488  sgn3da  34536  subfacp1lem5  35181  erdszelem7  35194  erdszelem11  35198  pconnconn  35228  txpconn  35229  connpconn  35232  sconnpi1  35236  txsconn  35238  cvxsconn  35240  cvmopnlem  35275  cvmfolem  35276  cvmliftmolem2  35279  cvmliftlem7  35288  cvmliftlem10  35291  cvmlift2lem10  35309  cvmlift3lem4  35319  cvmlift3lem8  35323  satfun  35408  msubff1  35553  wzel  35818  wsuclem  35819  btwnouttr2  36016  cgrxfr  36049  btwnxfr  36050  brcolinear  36053  lineext  36070  btwnconn1lem13  36093  midofsegid  36098  segcon2  36099  brsegle  36102  seglecgr12im  36104  segletr  36108  colinbtwnle  36112  broutsideof2  36116  btwnoutside  36119  broutsideof3  36120  outsideoftr  36123  outsideofeq  36124  outsideofeu  36125  outsidele  36126  lineunray  36141  lineelsb2  36142  linethru  36147  finminlem  36313  nn0prpwlem  36317  neibastop2lem  36355  neibastop2  36356  neibastop3  36357  topjoin  36360  tailfb  36372  relowlssretop  37358  fvineqsneq  37407  wl-sbcom2d-lem1  37552  finixpnum  37604  poimirlem6  37625  poimirlem7  37626  poimirlem13  37632  poimirlem26  37645  poimirlem29  37648  heicant  37654  opnmbllem0  37655  mblfinlem3  37658  ismblfin  37660  ovoliunnfl  37661  voliunnfl  37663  volsupnfl  37664  itg2addnclem  37670  itg2addnclem3  37672  ftc1cnnc  37691  sdclem2  37741  fdc  37744  istotbnd3  37770  isbnd2  37782  isbnd3  37783  prdsbnd  37792  cntotbnd  37795  heibor1lem  37808  heibor1  37809  heiborlem10  37819  rrncmslem  37831  ghomco  37890  1idl  38025  unichnidl  38030  disjlem18  38794  prtlem10  38859  prtlem18  38871  atlatmstc  39313  cvrexchlem  39414  paddasslem14  39828  pexmidlem5N  39969  cdleme29ex  40369  cdlemefr29exN  40397  cdleme32fva  40432  diarnN  41124  dihlsscpre  41229  isnacs3  42712  fnwe2lem2  43054  kelac1  43066  hbtlem5  43131  hbt  43133  dgraa0p  43152  ofoafg  43358  ofoafo  43360  naddcnffo  43368  fzunt  43459  fzuntd  43460  monoordxrv  45444  rlimdmafv  47138  rlimdmafv2  47219  fmtnoprmfac2  47503  perfectALTVlem2  47658  mogoldbb  47721  lindslinindsimp2  48330