Theorem expr 457

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  animpimp2impd  844  3expia  1121  rexlimdvaa  3155  reximddv  3170  disjxiun  5138  wereu2  5666  frpomin  6330  ordtr3  6398  fcof1  7269  knatar  7338  riota5f  7378  ovmpodf  7547  extmptsuppeq  8155  suppss  8161  suppssOLD  8162  suppss2  8167  frrlem14  8266  fprresex  8277  wfrlem17OLD  8307  smoord  8347  tfrlem9a  8368  oaass  8544  oelimcl  8583  oaabs2  8631  cofon1  8654  naddssim  8667  swoso  8719  eceqoveq  8799  domdifsn  9037  domunsncan  9055  omxpenlem  9056  enfixsn  9064  mapdom2  9131  frfi  9271  fofinf1o  9310  finsschain  9342  elfiun  9407  marypha1lem  9410  eqsupd  9434  eqinfd  9462  ordiso2  9492  ordtypelem6  9500  ordtypelem7  9501  ordtypelem10  9504  oismo  9517  wemapsolem  9527  brwdom2  9550  wdomtr  9552  unwdomg  9561  xpwdomg  9562  unxpwdom2  9565  cantnfval2  9646  cantnfle  9648  cantnflem1  9666  cantnf  9670  r1ordg  9755  tcrank  9861  carddomi2  9947  harval2  9974  infxpenlem  9990  infxpenc2lem2  9997  fseqenlem1  10001  dfac8clem  10009  acndom2  10031  infpwfien  10039  iunfictbso  10091  dfac12lem3  10122  infxp  10192  coflim  10238  cofsmo  10246  coftr  10250  sornom  10254  infpssrlem4  10283  enfin2i  10298  fin23lem26  10302  fin23lem27  10305  fin23lem36  10325  fin23lem40  10328  isf32lem5  10334  isf34lem4  10354  isfin1-3  10363  fin1a2lem10  10386  fin1a2lem13  10389  fin1a2s  10391  hsmexlem4  10406  ttukeylem5  10490  ttukeylem6  10491  ttukeylem7  10492  alephval2  10549  gchor  10604  fpwwe2lem6  10613  fpwwe2lem11  10618  fpwwe2  10620  pwfseqlem4a  10638  pwfseqlem4  10639  winalim2  10673  gchina  10676  inar1  10752  nqereq  10912  prlem934  11010  prlem936  11024  addsrmo  11050  mulsrmo  11051  supsrlem  11088  axpre-sup  11146  dedekind  11359  dedekindle  11360  mulge0b  12066  supaddc  12163  supmul1  12165  un0addcl  12487  un0mulcl  12488  uzwo3  12909  qbtwnre  13160  xlemul1a  13249  seqcl2  13968  seqfveq2  13972  seqshft2  13976  monoord  13980  seqsplit  13983  seqf1olem1  13989  seqid2  13996  seqhomo  13997  expnegz  14044  expcan  14116  ltexp2  14117  discr  14185  bcval5  14260  hashbc  14394  hashf1lem2  14399  seqcoll  14407  seqcoll2  14408  wrdind  14654  wrd2ind  14655  cau3lem  15283  ello1d  15449  lo1bdd2  15450  rlimclim  15472  climrlim2  15473  rlimdm  15477  rlimcn1  15514  reccn2  15523  rlimsqzlem  15577  lo1le  15580  caucvgrlem  15601  caurcvg2  15606  summolem2  15644  zsum  15646  fsum  15648  fsumf1o  15651  sumss  15652  fsumss  15653  fsumcl2lem  15659  fsumadd  15668  fsumcom2  15702  fsum0diag2  15711  fsummulc2  15712  fsumconst  15718  fsumrelem  15735  fsumrlim  15739  fsumo1  15740  divrcnv  15780  geomulcvg  15804  mertenslem2  15813  prodmolem2  15861  zprod  15863  fprod  15867  fprodf1o  15872  prodss  15873  fprodss  15874  fprodcl2lem  15876  fprodmul  15886  fproddiv  15887  fprodconst  15904  fprodn0  15905  fprodcom2  15910  ruclem8  16162  dvds0lem  16192  dvdsnegb  16199  dvdssub2  16226  bitsf1  16369  bitsshft  16398  bezoutlem3  16465  bezoutlem4  16466  isprm5  16626  isprm6  16633  hashgcdeq  16704  modprminv  16714  modprminveq  16715  reumodprminv  16719  pcqmul  16768  pcqcl  16771  pcxnn0cl  16775  pcxcl  16776  pc2dvds  16794  pcadd  16804  pcmpt  16807  pockthg  16821  infpnlem1  16825  prmreclem5  16835  vdwlem2  16897  vdwlem9  16904  vdwlem10  16905  vdwlem12  16907  ramub  16928  0ram  16935  ramub1lem2  16942  ramub1  16943  ramcl  16944  mreexexd  17574  acsfn2  17589  iscatd  17599  catpropd  17635  setcmon  18019  pleval2i  18271  psss  18515  mgmidsssn0  18573  mhmeql  18682  frmdss2  18719  frmdup3  18723  grprcan  18833  dfgrp3lem  18895  mulgnn0ass  18962  isnsg3  19012  ghmpreima  19080  ghmeql  19081  gaorber  19138  f1omvdco2  19280  psgnunilem1  19325  psgnunilem2  19327  oddvds  19379  gexdvds  19416  sylow1lem1  19430  odcau  19436  pgpssslw  19446  sylow2alem2  19450  sylow2blem3  19454  fislw  19457  lsmmod  19507  efgredlem  19579  frgpup3  19610  gsumval3  19734  gsumzres  19736  gsumzcl2  19737  gsumzf1o  19739  gsumzaddlem  19748  gsumconst  19761  gsumzmhm  19764  gsumzoppg  19771  gsum2d2lem  19800  ablfac1eulem  19901  pgpfac1lem5  19908  ablfaclem3  19916  issubdrg  20338  lss1d  20523  lmhmeql  20615  lspextmo  20616  lspsnat  20707  lsppratlem6  20714  islbs3  20717  lbsextlem4  20723  lidl1el  20789  cnsubrg  20939  gsumfsum  20946  prmirredlem  20975  znidomb  21050  frgpcyg  21062  cssmre  21179  dsmmsubg  21231  dsmmlss  21232  frlmsslsp  21284  lindff1  21308  lindfrn  21309  rnasclassa  21380  mvrf1  21476  mplsubglem  21487  mpllsslem  21488  mplcoe1  21520  mplcoe5  21523  gsummoncoe1  21757  mat1dimcrng  21908  mdetdiaglem  22029  mdetunilem7  22049  mdetunilem8  22050  mdetunilem9  22051  cpmatacl  22147  cpmatmcllem  22149  mp2pm2mplem4  22240  en2top  22417  toponmre  22526  topssnei  22557  innei  22558  clslp  22581  restcls  22614  restntr  22615  ordtrest2lem  22636  cnpco  22700  cncls2  22706  cncnpi  22711  cncnp  22713  cnconst2  22716  cnpdis  22726  lmcnp  22737  cnhaus  22787  isreg2  22810  cncmp  22825  tgcmp  22834  sscmp  22838  cmpfi  22841  cnconn  22855  iunconnlem  22860  clsconn  22863  1stcfb  22878  1stcrest  22886  2ndcctbss  22888  2ndcdisj  22889  1stcelcls  22894  1stccnp  22895  restnlly  22915  cldllycmp  22928  lly1stc  22929  dislly  22930  locfincmp  22959  comppfsc  22965  kgentopon  22971  kgenidm  22980  1stckgenlem  22986  kgencn3  22991  ptpjpre1  23004  ptbasin  23010  txcls  23037  tx2cn  23043  ptpjcn  23044  ptclsg  23048  ptcnp  23055  txdis  23065  txlly  23069  txnlly  23070  pthaus  23071  txtube  23073  txcmplem1  23074  txcmplem2  23075  txcmp  23076  txhaus  23080  txkgen  23085  xkohaus  23086  xkococnlem  23092  xkococn  23093  txconn  23122  qtopeu  23149  qtoprest  23150  regr1lem2  23173  kqreglem1  23174  cmphaushmeo  23233  xkocnv  23247  fgabs  23312  filuni  23318  trufil  23343  ufileu  23352  filufint  23353  fin1aufil  23365  elfm2  23381  rnelfmlem  23385  fmfnfmlem2  23388  fmfnfmlem4  23390  fmufil  23392  flimopn  23408  fbflim2  23410  hausflimi  23413  hausflim  23414  flimcf  23415  flimclslem  23417  flimsncls  23419  hauspwpwf1  23420  cnpflfi  23432  fclsnei  23452  fclscf  23458  flimfnfcls  23461  fclscmp  23463  ufilcmp  23465  fcfnei  23468  cnpfcf  23474  alexsublem  23477  alexsub  23478  alexsubALTlem2  23481  alexsubALTlem3  23482  alexsubALTlem4  23483  ptcmplem3  23487  ptcmplem4  23488  ptcmplem5  23489  symgtgp  23539  tgpconncompeqg  23545  tgpconncomp  23546  ghmcnp  23548  tgpt0  23552  qustgplem  23554  haustsms2  23570  tsmsgsum  23572  tsmsres  23577  tsmsxp  23588  imasdsf1olem  23808  xbln0  23849  blssps  23859  blss  23860  neibl  23939  blcld  23943  metss  23946  metequiv2  23948  met1stc  23959  metrest  23962  prdsxmslem2  23967  metcnp3  23978  nrmmetd  24012  nlmvscnlem1  24132  nrginvrcnlem  24137  nmoleub  24177  icccmplem2  24268  icccmp  24270  reconnlem2  24272  xrge0tsms  24279  metdstri  24296  metdseq0  24299  metdscn  24301  cnmpopc  24373  lebnumlem3  24408  pcoval2  24461  pcopt  24467  nmoleub2lem  24559  nmhmcn  24565  ipcnlem1  24691  cfilfcls  24720  cmetcaulem  24734  iscmet3lem2  24738  iscmet3  24739  equivcau  24746  caubl  24754  bcthlem2  24771  bcthlem3  24772  bcthlem4  24773  bcthlem5  24774  ivthlem2  24898  ivthlem3  24899  ovoliunlem2  24949  ovolicc2lem2  24964  ovolicc2lem5  24967  ovolicc2  24968  ismbl2  24973  nulmbl  24981  nulmbl2  24982  unmbl  24983  shftmbl  24984  voliunlem3  24998  volsup  25002  ioombl1lem4  25007  ioombl1  25008  icombl  25010  ioombl  25011  uniioombl  25035  opnmbllem  25047  volivth  25053  vitali  25059  mbflimsup  25112  i1fadd  25141  itg1addlem4  25145  itg1addlem4OLD  25146  itg2le  25186  itg2seq  25189  itg2lea  25191  itg2splitlem  25195  itg2split  25196  itg2mono  25200  itg2gt0  25207  itg2cnlem2  25209  itgss  25258  itgfsum  25273  itgcn  25291  ellimc3  25325  limcco  25339  limciun  25340  dvnres  25377  dvnfre  25398  rolle  25436  c1liplem1  25442  dvivth  25456  dvne0  25457  lhop1lem  25459  lhop1  25460  lhop  25462  dvcnvrelem1  25463  dvfsumrlim  25477  dvfsum2  25480  ftc1a  25483  ftc1lem6  25487  itgsubst  25495  tdeglem4  25506  tdeglem4OLD  25507  mdegaddle  25521  mdegvscale  25522  mdegmullem  25525  deg1tmle  25564  ply1divex  25583  dvdsq1p  25607  fta1g  25614  fta1b  25616  plyco0  25635  coeeulem  25667  dgrlem  25672  plyco  25684  coemullem  25693  dgreq0  25708  dgrco  25718  plydivex  25739  quotcan  25751  aannenlem1  25770  aalioulem2  25775  aalioulem3  25776  taylthlem1  25814  ulmbdd  25839  itgulm  25849  radcnvlt1  25859  psercnlem1  25866  abelthlem2  25873  abelthlem8  25880  logcnlem5  26083  efopn  26095  cxpmul2z  26128  cxpcn3lem  26182  cxpeq  26192  xrlimcnp  26400  cxplim  26403  o1cxp  26406  cxploglim  26409  scvxcvx  26417  jensen  26420  ftalem1  26504  ftalem2  26505  fta  26511  basellem3  26514  isppw2  26546  ppinprm  26583  chtnprm  26585  dvdsmulf1o  26625  chtublem  26641  perfectlem2  26660  dchrfi  26685  dchrptlem1  26694  dchrptlem2  26695  dchrptlem3  26696  dchrsum2  26698  bposlem1  26714  bposlem3  26716  2sqlem5  26852  2sqlem6  26853  2sqlem8  26856  2sqlem10  26858  2sqb  26862  chebbnd1lem1  26899  chtppilimlem2  26904  dchrisum0flb  26940  dchrisum0fno1  26941  dchrisum0  26950  pntrsumbnd2  26997  pntpbnd1  27016  pntpbnd2  27017  pntlemp  27040  pnt3  27042  qabvle  27055  ostth2lem2  27064  ostth3  27068  ostth  27069  nolt02o  27125  nogt01o  27126  nosupprefixmo  27130  noinfprefixmo  27131  nosupbnd1lem3  27140  nosupbnd1lem4  27141  nosupbnd1lem5  27142  noinfbnd1lem3  27155  noinfbnd1lem4  27156  noinfbnd1lem5  27157  noetasuplem4  27166  noetainflem4  27170  etasslt  27240  madebdaylemlrcut  27316  mulsuniflem  27516  colinearalglem4  28032  axcontlem10  28096  upgrex  28217  smcnlem  29813  ubthlem1  29986  ubthlem3  29988  htthlem  30033  5oalem6  30775  leopmuli  31249  pjnormssi  31284  pjclem4  31315  pj3si  31323  hatomistici  31478  sumdmdlem  31534  wrdt2ind  31988  xrge0tsmsd  32080  isarchiofld  32297  ordtrest2NEWlem  32733  qqhf  32797  eulerpartlemb  33198  ballotlemfc0  33322  ballotlemfcc  33323  sgn3da  33371  subfacp1lem5  34006  erdszelem7  34019  erdszelem11  34023  pconnconn  34053  txpconn  34054  connpconn  34057  sconnpi1  34061  txsconn  34063  cvxsconn  34065  cvmopnlem  34100  cvmfolem  34101  cvmliftmolem2  34104  cvmliftlem7  34113  cvmliftlem10  34116  cvmlift2lem10  34134  cvmlift3lem4  34144  cvmlift3lem8  34148  satfun  34233  msubff1  34378  wzel  34626  wsuclem  34627  btwnouttr2  34824  cgrxfr  34857  btwnxfr  34858  brcolinear  34861  lineext  34878  btwnconn1lem13  34901  midofsegid  34906  segcon2  34907  brsegle  34910  seglecgr12im  34912  segletr  34916  colinbtwnle  34920  broutsideof2  34924  btwnoutside  34927  broutsideof3  34928  outsideoftr  34931  outsideofeq  34932  outsideofeu  34933  outsidele  34934  lineunray  34949  lineelsb2  34950  linethru  34955  finminlem  35007  nn0prpwlem  35011  neibastop2lem  35049  neibastop2  35050  neibastop3  35051  topjoin  35054  tailfb  35066  relowlssretop  36048  fvineqsneq  36097  wl-sbcom2d-lem1  36228  finixpnum  36277  poimirlem6  36298  poimirlem7  36299  poimirlem13  36305  poimirlem26  36318  poimirlem29  36321  heicant  36327  opnmbllem0  36328  mblfinlem3  36331  ismblfin  36333  ovoliunnfl  36334  voliunnfl  36336  volsupnfl  36337  itg2addnclem  36343  itg2addnclem3  36345  ftc1cnnc  36364  sdclem2  36415  fdc  36418  istotbnd3  36444  isbnd2  36456  isbnd3  36457  prdsbnd  36466  cntotbnd  36469  heibor1lem  36482  heibor1  36483  heiborlem10  36493  rrncmslem  36505  ghomco  36564  1idl  36699  unichnidl  36704  disjlem18  37475  prtlem10  37540  prtlem18  37552  atlatmstc  37994  cvrexchlem  38095  paddasslem14  38509  pexmidlem5N  38650  cdleme29ex  39050  cdlemefr29exN  39078  cdleme32fva  39113  diarnN  39805  dihlsscpre  39910  isnacs3  41219  fnwe2lem2  41564  kelac1  41576  hbtlem5  41641  hbt  41643  dgraa0p  41662  ofoafg  41875  ofoafo  41877  naddcnffo  41885  fzunt  41977  fzuntd  41978  monoordxrv  43965  rlimdmafv  45657  rlimdmafv2  45738  fmtnoprmfac2  46007  perfectALTVlem2  46162  mogoldbb  46225  mgmhmeql  46345  lindslinindsimp2  46792