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  845  3expia  1121  rexlimdvaa  3162  reximddv  3177  disjxiun  5163  wereu2  5697  frpomin  6372  ordtr3  6440  fcof1  7323  knatar  7393  riota5f  7433  ovmpodf  7606  extmptsuppeq  8229  suppss  8235  suppss2  8241  frrlem14  8340  fprresex  8351  wfrlem17OLD  8381  smoord  8421  tfrlem9a  8442  oaass  8617  oelimcl  8656  oaabs2  8705  cofon1  8728  naddssim  8741  swoso  8797  eceqoveq  8880  domdifsn  9120  domunsncan  9138  omxpenlem  9139  enfixsn  9147  mapdom2  9214  frfi  9349  fofinf1o  9400  finsschain  9429  elfiun  9499  marypha1lem  9502  eqsupd  9526  eqinfd  9554  ordiso2  9584  ordtypelem6  9592  ordtypelem7  9593  ordtypelem10  9596  oismo  9609  wemapsolem  9619  brwdom2  9642  wdomtr  9644  unwdomg  9653  xpwdomg  9654  unxpwdom2  9657  cantnfval2  9738  cantnfle  9740  cantnflem1  9758  cantnf  9762  r1ordg  9847  tcrank  9953  carddomi2  10039  harval2  10066  infxpenlem  10082  infxpenc2lem2  10089  fseqenlem1  10093  dfac8clem  10101  acndom2  10123  infpwfien  10131  iunfictbso  10183  dfac12lem3  10215  infxp  10283  coflim  10330  cofsmo  10338  coftr  10342  sornom  10346  infpssrlem4  10375  enfin2i  10390  fin23lem26  10394  fin23lem27  10397  fin23lem36  10417  fin23lem40  10420  isf32lem5  10426  isf34lem4  10446  isfin1-3  10455  fin1a2lem10  10478  fin1a2lem13  10481  fin1a2s  10483  hsmexlem4  10498  ttukeylem5  10582  ttukeylem6  10583  ttukeylem7  10584  alephval2  10641  gchor  10696  fpwwe2lem6  10705  fpwwe2lem11  10710  fpwwe2  10712  pwfseqlem4a  10730  pwfseqlem4  10731  winalim2  10765  gchina  10768  inar1  10844  nqereq  11004  prlem934  11102  prlem936  11116  addsrmo  11142  mulsrmo  11143  supsrlem  11180  axpre-sup  11238  dedekind  11453  dedekindle  11454  mulge0b  12165  supaddc  12262  supmul1  12264  un0addcl  12586  un0mulcl  12587  uzwo3  13008  qbtwnre  13261  xlemul1a  13350  seqcl2  14071  seqfveq2  14075  seqshft2  14079  monoord  14083  seqsplit  14086  seqf1olem1  14092  seqid2  14099  seqhomo  14100  expnegz  14147  expcan  14219  ltexp2  14220  discr  14289  bcval5  14367  hashbc  14502  hashf1lem2  14505  seqcoll  14513  seqcoll2  14514  wrdind  14770  wrd2ind  14771  cau3lem  15403  ello1d  15569  lo1bdd2  15570  rlimclim  15592  climrlim2  15593  rlimdm  15597  rlimcn1  15634  reccn2  15643  rlimsqzlem  15697  lo1le  15700  caucvgrlem  15721  caurcvg2  15726  summolem2  15764  zsum  15766  fsum  15768  fsumf1o  15771  sumss  15772  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  fsumcom2  15822  fsum0diag2  15831  fsummulc2  15832  fsumconst  15838  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  divrcnv  15900  geomulcvg  15924  mertenslem2  15933  prodmolem2  15983  zprod  15985  fprod  15989  fprodf1o  15994  prodss  15995  fprodss  15996  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodconst  16026  fprodn0  16027  fprodcom2  16032  ruclem8  16285  dvds0lem  16315  dvdsnegb  16322  dvdssub2  16349  bitsf1  16492  bitsshft  16521  bezoutlem3  16588  bezoutlem4  16589  isprm5  16754  isprm6  16761  hashgcdeq  16836  modprminv  16846  modprminveq  16847  reumodprminv  16851  pcqmul  16900  pcqcl  16903  pcxnn0cl  16907  pcxcl  16908  pc2dvds  16926  pcadd  16936  pcmpt  16939  pockthg  16953  infpnlem1  16957  prmreclem5  16967  vdwlem2  17029  vdwlem9  17036  vdwlem10  17037  vdwlem12  17039  ramub  17060  0ram  17067  ramub1lem2  17074  ramub1  17075  ramcl  17076  mreexexd  17706  acsfn2  17721  iscatd  17731  catpropd  17767  setcmon  18154  pleval2i  18406  psss  18650  mgmidsssn0  18710  mgmhmeql  18754  mhmeql  18861  frmdss2  18898  frmdup3  18902  grprcan  19013  dfgrp3lem  19078  mulgnn0ass  19150  isnsg3  19200  ghmpreima  19278  ghmeql  19279  gaorber  19348  f1omvdco2  19490  psgnunilem1  19535  psgnunilem2  19537  oddvds  19589  gexdvds  19626  sylow1lem1  19640  odcau  19646  pgpssslw  19656  sylow2alem2  19660  sylow2blem3  19664  fislw  19667  lsmmod  19717  efgredlem  19789  frgpup3  19820  gsumval3  19949  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  gsum2d2lem  20015  ablfac1eulem  20116  pgpfac1lem5  20123  ablfaclem3  20131  issubdrg  20803  lss1d  20984  lmhmeql  21077  lspextmo  21078  lspsnat  21170  lsppratlem6  21177  islbs3  21180  lbsextlem4  21186  lidl1el  21259  cnsubrg  21468  gsumfsum  21475  prmirredlem  21506  znidomb  21603  frgpcyg  21615  cssmre  21734  dsmmsubg  21786  dsmmlss  21787  frlmsslsp  21839  lindff1  21863  lindfrn  21864  rnasclassa  21938  mvrf1  22029  mplsubglem  22042  mpllsslem  22043  mplcoe1  22078  mplcoe5  22081  gsummoncoe1  22333  mat1dimcrng  22504  mdetdiaglem  22625  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  cpmatacl  22743  cpmatmcllem  22745  mp2pm2mplem4  22836  en2top  23013  toponmre  23122  topssnei  23153  innei  23154  clslp  23177  restcls  23210  restntr  23211  ordtrest2lem  23232  cnpco  23296  cncls2  23302  cncnpi  23307  cncnp  23309  cnconst2  23312  cnpdis  23322  lmcnp  23333  cnhaus  23383  isreg2  23406  cncmp  23421  tgcmp  23430  sscmp  23434  cmpfi  23437  cnconn  23451  iunconnlem  23456  clsconn  23459  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  2ndcdisj  23485  1stcelcls  23490  1stccnp  23491  restnlly  23511  cldllycmp  23524  lly1stc  23525  dislly  23526  locfincmp  23555  comppfsc  23561  kgentopon  23567  kgenidm  23576  1stckgenlem  23582  kgencn3  23587  ptpjpre1  23600  ptbasin  23606  txcls  23633  tx2cn  23639  ptpjcn  23640  ptclsg  23644  ptcnp  23651  txdis  23661  txlly  23665  txnlly  23666  pthaus  23667  txtube  23669  txcmplem1  23670  txcmplem2  23671  txcmp  23672  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  xkococn  23689  txconn  23718  qtopeu  23745  qtoprest  23746  regr1lem2  23769  kqreglem1  23770  cmphaushmeo  23829  xkocnv  23843  fgabs  23908  filuni  23914  trufil  23939  ufileu  23948  filufint  23949  fin1aufil  23961  elfm2  23977  rnelfmlem  23981  fmfnfmlem2  23984  fmfnfmlem4  23986  fmufil  23988  flimopn  24004  fbflim2  24006  hausflimi  24009  hausflim  24010  flimcf  24011  flimclslem  24013  flimsncls  24015  hauspwpwf1  24016  cnpflfi  24028  fclsnei  24048  fclscf  24054  flimfnfcls  24057  fclscmp  24059  ufilcmp  24061  fcfnei  24064  cnpfcf  24070  alexsublem  24073  alexsub  24074  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem4  24084  ptcmplem5  24085  symgtgp  24135  tgpconncompeqg  24141  tgpconncomp  24142  ghmcnp  24144  tgpt0  24148  qustgplem  24150  haustsms2  24166  tsmsgsum  24168  tsmsres  24173  tsmsxp  24184  imasdsf1olem  24404  xbln0  24445  blssps  24455  blss  24456  neibl  24535  blcld  24539  metss  24542  metequiv2  24544  met1stc  24555  metrest  24558  prdsxmslem2  24563  metcnp3  24574  nrmmetd  24608  nlmvscnlem1  24728  nrginvrcnlem  24733  nmoleub  24773  icccmplem2  24864  icccmp  24866  reconnlem2  24868  xrge0tsms  24875  metdstri  24892  metdseq0  24895  metdscn  24897  cnmpopc  24974  lebnumlem3  25014  pcoval2  25068  pcopt  25074  nmoleub2lem  25166  nmhmcn  25172  ipcnlem1  25298  cfilfcls  25327  cmetcaulem  25341  iscmet3lem2  25345  iscmet3  25346  equivcau  25353  caubl  25361  bcthlem2  25378  bcthlem3  25379  bcthlem4  25380  bcthlem5  25381  ivthlem2  25506  ivthlem3  25507  ovoliunlem2  25557  ovolicc2lem2  25572  ovolicc2lem5  25575  ovolicc2  25576  ismbl2  25581  nulmbl  25589  nulmbl2  25590  unmbl  25591  shftmbl  25592  voliunlem3  25606  volsup  25610  ioombl1lem4  25615  ioombl1  25616  icombl  25618  ioombl  25619  uniioombl  25643  opnmbllem  25655  volivth  25661  vitali  25667  mbflimsup  25720  i1fadd  25749  itg1addlem4  25753  itg1addlem4OLD  25754  itg2le  25794  itg2seq  25797  itg2lea  25799  itg2splitlem  25803  itg2split  25804  itg2mono  25808  itg2gt0  25815  itg2cnlem2  25817  itgss  25867  itgfsum  25882  itgcn  25900  ellimc3  25934  limcco  25948  limciun  25949  dvnres  25987  dvnfre  26010  rolle  26048  c1liplem1  26055  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop1  26073  lhop  26075  dvcnvrelem1  26076  dvfsumrlim  26092  dvfsum2  26095  ftc1a  26098  ftc1lem6  26102  itgsubst  26110  tdeglem4  26119  mdegaddle  26133  mdegvscale  26134  mdegmullem  26137  deg1tmle  26177  ply1divex  26196  dvdsq1p  26222  fta1g  26229  fta1b  26231  plyco0  26251  coeeulem  26283  dgrlem  26288  plyco  26300  coemullem  26309  dgreq0  26325  dgrco  26335  plydivex  26357  quotcan  26369  aannenlem1  26388  aalioulem2  26393  aalioulem3  26394  taylthlem1  26433  ulmbdd  26459  itgulm  26469  radcnvlt1  26479  psercnlem1  26487  abelthlem2  26494  abelthlem8  26501  logcnlem5  26706  efopn  26718  cxpmul2z  26751  cxpcn3lem  26808  cxpeq  26818  xrlimcnp  27029  cxplim  27033  o1cxp  27036  cxploglim  27039  scvxcvx  27047  jensen  27050  ftalem1  27134  ftalem2  27135  fta  27141  basellem3  27144  isppw2  27176  ppinprm  27213  chtnprm  27215  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chtublem  27273  perfectlem2  27292  dchrfi  27317  dchrptlem1  27326  dchrptlem2  27327  dchrptlem3  27328  dchrsum2  27330  bposlem1  27346  bposlem3  27348  2sqlem5  27484  2sqlem6  27485  2sqlem8  27488  2sqlem10  27490  2sqb  27494  chebbnd1lem1  27531  chtppilimlem2  27536  dchrisum0flb  27572  dchrisum0fno1  27573  dchrisum0  27582  pntrsumbnd2  27629  pntpbnd1  27648  pntpbnd2  27649  pntlemp  27672  pnt3  27674  qabvle  27687  ostth2lem2  27696  ostth3  27700  ostth  27701  nolt02o  27758  nogt01o  27759  nosupprefixmo  27763  noinfprefixmo  27764  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  etasslt  27876  cuteq1  27896  madebdaylemlrcut  27955  cutlt  27984  mulsuniflem  28193  om2noseqlt  28323  readdscl  28449  remulscl  28452  colinearalglem4  28942  axcontlem10  29006  upgrex  29127  smcnlem  30729  ubthlem1  30902  ubthlem3  30904  htthlem  30949  5oalem6  31691  leopmuli  32165  pjnormssi  32200  pjclem4  32231  pj3si  32239  hatomistici  32394  sumdmdlem  32450  wrdt2ind  32920  xrge0tsmsd  33041  isarchiofld  33312  ordtrest2NEWlem  33868  qqhf  33932  eulerpartlemb  34333  ballotlemfc0  34457  ballotlemfcc  34458  sgn3da  34506  subfacp1lem5  35152  erdszelem7  35165  erdszelem11  35169  pconnconn  35199  txpconn  35200  connpconn  35203  sconnpi1  35207  txsconn  35209  cvxsconn  35211  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem10  35280  cvmlift3lem4  35290  cvmlift3lem8  35294  satfun  35379  msubff1  35524  wzel  35788  wsuclem  35789  btwnouttr2  35986  cgrxfr  36019  btwnxfr  36020  brcolinear  36023  lineext  36040  btwnconn1lem13  36063  midofsegid  36068  segcon2  36069  brsegle  36072  seglecgr12im  36074  segletr  36078  colinbtwnle  36082  broutsideof2  36086  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsideofeq  36094  outsideofeu  36095  outsidele  36096  lineunray  36111  lineelsb2  36112  linethru  36117  finminlem  36284  nn0prpwlem  36288  neibastop2lem  36326  neibastop2  36327  neibastop3  36328  topjoin  36331  tailfb  36343  relowlssretop  37329  fvineqsneq  37378  wl-sbcom2d-lem1  37513  finixpnum  37565  poimirlem6  37586  poimirlem7  37587  poimirlem13  37593  poimirlem26  37606  poimirlem29  37609  heicant  37615  opnmbllem0  37616  mblfinlem3  37619  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  itg2addnclem3  37633  ftc1cnnc  37652  sdclem2  37702  fdc  37705  istotbnd3  37731  isbnd2  37743  isbnd3  37744  prdsbnd  37753  cntotbnd  37756  heibor1lem  37769  heibor1  37770  heiborlem10  37780  rrncmslem  37792  ghomco  37851  1idl  37986  unichnidl  37991  disjlem18  38756  prtlem10  38821  prtlem18  38833  atlatmstc  39275  cvrexchlem  39376  paddasslem14  39790  pexmidlem5N  39931  cdleme29ex  40331  cdlemefr29exN  40359  cdleme32fva  40394  diarnN  41086  dihlsscpre  41191  isnacs3  42666  fnwe2lem2  43008  kelac1  43020  hbtlem5  43085  hbt  43087  dgraa0p  43106  ofoafg  43316  ofoafo  43318  naddcnffo  43326  fzunt  43417  fzuntd  43418  monoordxrv  45397  rlimdmafv  47092  rlimdmafv2  47173  fmtnoprmfac2  47441  perfectALTVlem2  47596  mogoldbb  47659  lindslinindsimp2  48192