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  3137  reximddv  3151  disjxiun  5112  wereu2  5643  frpomin  6321  ordtr3  6386  fcof1  7269  knatar  7339  riota5f  7379  ovmpodf  7552  extmptsuppeq  8176  suppss  8182  suppss2  8188  frrlem14  8287  fprresex  8298  smoord  8343  tfrlem9a  8363  oaass  8536  oelimcl  8575  oaabs2  8624  cofon1  8647  naddssim  8660  swoso  8716  eceqoveq  8799  domdifsn  9031  domunsncan  9049  omxpenlem  9050  enfixsn  9058  mapdom2  9125  frfi  9250  fofinf1o  9301  finsschain  9328  elfiun  9399  marypha1lem  9402  eqsupd  9426  eqinfd  9455  ordiso2  9486  ordtypelem6  9494  ordtypelem7  9495  ordtypelem10  9498  oismo  9511  wemapsolem  9521  brwdom2  9544  wdomtr  9546  unwdomg  9555  xpwdomg  9556  unxpwdom2  9559  cantnfval2  9640  cantnfle  9642  cantnflem1  9660  cantnf  9664  r1ordg  9749  tcrank  9855  carddomi2  9941  harval2  9968  infxpenlem  9984  infxpenc2lem2  9991  fseqenlem1  9995  dfac8clem  10003  acndom2  10025  infpwfien  10033  iunfictbso  10085  dfac12lem3  10117  infxp  10185  coflim  10232  cofsmo  10240  coftr  10244  sornom  10248  infpssrlem4  10277  enfin2i  10292  fin23lem26  10296  fin23lem27  10299  fin23lem36  10319  fin23lem40  10322  isf32lem5  10328  isf34lem4  10348  isfin1-3  10357  fin1a2lem10  10380  fin1a2lem13  10383  fin1a2s  10385  hsmexlem4  10400  ttukeylem5  10484  ttukeylem6  10485  ttukeylem7  10486  alephval2  10543  gchor  10598  fpwwe2lem6  10607  fpwwe2lem11  10612  fpwwe2  10614  pwfseqlem4a  10632  pwfseqlem4  10633  winalim2  10667  gchina  10670  inar1  10746  nqereq  10906  prlem934  11004  prlem936  11018  addsrmo  11044  mulsrmo  11045  supsrlem  11082  axpre-sup  11140  dedekind  11355  dedekindle  11356  mulge0b  12069  supaddc  12166  supmul1  12168  un0addcl  12491  un0mulcl  12492  uzwo3  12916  qbtwnre  13172  xlemul1a  13261  seqcl2  13995  seqfveq2  13999  seqshft2  14003  monoord  14007  seqsplit  14010  seqf1olem1  14016  seqid2  14023  seqhomo  14024  expnegz  14071  expcan  14144  ltexp2  14145  discr  14215  bcval5  14293  hashbc  14428  hashf1lem2  14431  seqcoll  14439  seqcoll2  14440  wrdind  14697  wrd2ind  14698  cau3lem  15330  ello1d  15496  lo1bdd2  15497  rlimclim  15519  climrlim2  15520  rlimdm  15524  rlimcn1  15561  reccn2  15570  rlimsqzlem  15622  lo1le  15625  caucvgrlem  15646  caurcvg2  15651  summolem2  15689  zsum  15691  fsum  15693  fsumf1o  15696  sumss  15697  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsumcom2  15747  fsum0diag2  15756  fsummulc2  15757  fsumconst  15763  fsumrelem  15780  fsumrlim  15784  fsumo1  15785  divrcnv  15825  geomulcvg  15849  mertenslem2  15858  prodmolem2  15908  zprod  15910  fprod  15914  fprodf1o  15919  prodss  15920  fprodss  15921  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodconst  15951  fprodn0  15952  fprodcom2  15957  ruclem8  16212  dvds0lem  16243  dvdsnegb  16250  dvdssub2  16277  bitsf1  16422  bitsshft  16451  bezoutlem3  16517  bezoutlem4  16518  isprm5  16683  isprm6  16690  hashgcdeq  16766  modprminv  16776  modprminveq  16777  reumodprminv  16781  pcqmul  16830  pcqcl  16833  pcxnn0cl  16837  pcxcl  16838  pc2dvds  16856  pcadd  16866  pcmpt  16869  pockthg  16883  infpnlem1  16887  prmreclem5  16897  vdwlem2  16959  vdwlem9  16966  vdwlem10  16967  vdwlem12  16969  ramub  16990  0ram  16997  ramub1lem2  17004  ramub1  17005  ramcl  17006  mreexexd  17615  acsfn2  17630  iscatd  17640  catpropd  17676  setcmon  18055  pleval2i  18301  psss  18545  mgmidsssn0  18605  mgmhmeql  18649  mhmeql  18759  frmdss2  18796  frmdup3  18800  grprcan  18911  dfgrp3lem  18976  mulgnn0ass  19048  isnsg3  19098  ghmpreima  19176  ghmeql  19177  gaorber  19246  f1omvdco2  19384  psgnunilem1  19429  psgnunilem2  19431  oddvds  19483  gexdvds  19520  sylow1lem1  19534  odcau  19540  pgpssslw  19550  sylow2alem2  19554  sylow2blem3  19558  fislw  19561  lsmmod  19611  efgredlem  19683  frgpup3  19714  gsumval3  19843  gsumzres  19845  gsumzcl2  19846  gsumzf1o  19848  gsumzaddlem  19857  gsumconst  19870  gsumzmhm  19873  gsumzoppg  19880  gsum2d2lem  19909  ablfac1eulem  20010  pgpfac1lem5  20017  ablfaclem3  20025  issubdrg  20695  lss1d  20875  lmhmeql  20968  lspextmo  20969  lspsnat  21061  lsppratlem6  21068  islbs3  21071  lbsextlem4  21077  lidl1el  21142  cnsubrg  21350  gsumfsum  21357  prmirredlem  21388  znidomb  21477  frgpcyg  21489  cssmre  21608  dsmmsubg  21658  dsmmlss  21659  frlmsslsp  21711  lindff1  21735  lindfrn  21736  rnasclassa  21810  mvrf1  21901  mplsubglem  21914  mpllsslem  21915  mplcoe1  21950  mplcoe5  21953  gsummoncoe1  22201  mat1dimcrng  22370  mdetdiaglem  22491  mdetunilem7  22511  mdetunilem8  22512  mdetunilem9  22513  cpmatacl  22609  cpmatmcllem  22611  mp2pm2mplem4  22702  en2top  22878  toponmre  22986  topssnei  23017  innei  23018  clslp  23041  restcls  23074  restntr  23075  ordtrest2lem  23096  cnpco  23160  cncls2  23166  cncnpi  23171  cncnp  23173  cnconst2  23176  cnpdis  23186  lmcnp  23197  cnhaus  23247  isreg2  23270  cncmp  23285  tgcmp  23294  sscmp  23298  cmpfi  23301  cnconn  23315  iunconnlem  23320  clsconn  23323  1stcfb  23338  1stcrest  23346  2ndcctbss  23348  2ndcdisj  23349  1stcelcls  23354  1stccnp  23355  restnlly  23375  cldllycmp  23388  lly1stc  23389  dislly  23390  locfincmp  23419  comppfsc  23425  kgentopon  23431  kgenidm  23440  1stckgenlem  23446  kgencn3  23451  ptpjpre1  23464  ptbasin  23470  txcls  23497  tx2cn  23503  ptpjcn  23504  ptclsg  23508  ptcnp  23515  txdis  23525  txlly  23529  txnlly  23530  pthaus  23531  txtube  23533  txcmplem1  23534  txcmplem2  23535  txcmp  23536  txhaus  23540  txkgen  23545  xkohaus  23546  xkococnlem  23552  xkococn  23553  txconn  23582  qtopeu  23609  qtoprest  23610  regr1lem2  23633  kqreglem1  23634  cmphaushmeo  23693  xkocnv  23707  fgabs  23772  filuni  23778  trufil  23803  ufileu  23812  filufint  23813  fin1aufil  23825  elfm2  23841  rnelfmlem  23845  fmfnfmlem2  23848  fmfnfmlem4  23850  fmufil  23852  flimopn  23868  fbflim2  23870  hausflimi  23873  hausflim  23874  flimcf  23875  flimclslem  23877  flimsncls  23879  hauspwpwf1  23880  cnpflfi  23892  fclsnei  23912  fclscf  23918  flimfnfcls  23921  fclscmp  23923  ufilcmp  23925  fcfnei  23928  cnpfcf  23934  alexsublem  23937  alexsub  23938  alexsubALTlem2  23941  alexsubALTlem3  23942  alexsubALTlem4  23943  ptcmplem3  23947  ptcmplem4  23948  ptcmplem5  23949  symgtgp  23999  tgpconncompeqg  24005  tgpconncomp  24006  ghmcnp  24008  tgpt0  24012  qustgplem  24014  haustsms2  24030  tsmsgsum  24032  tsmsres  24037  tsmsxp  24048  imasdsf1olem  24267  xbln0  24308  blssps  24318  blss  24319  neibl  24395  blcld  24399  metss  24402  metequiv2  24404  met1stc  24415  metrest  24418  prdsxmslem2  24423  metcnp3  24434  nrmmetd  24468  nlmvscnlem1  24580  nrginvrcnlem  24585  nmoleub  24625  icccmplem2  24718  icccmp  24720  reconnlem2  24722  xrge0tsms  24729  metdstri  24746  metdseq0  24749  metdscn  24751  cnmpopc  24828  lebnumlem3  24868  pcoval2  24922  pcopt  24928  nmoleub2lem  25020  nmhmcn  25026  ipcnlem1  25152  cfilfcls  25181  cmetcaulem  25195  iscmet3lem2  25199  iscmet3  25200  equivcau  25207  caubl  25215  bcthlem2  25232  bcthlem3  25233  bcthlem4  25234  bcthlem5  25235  ivthlem2  25360  ivthlem3  25361  ovoliunlem2  25411  ovolicc2lem2  25426  ovolicc2lem5  25429  ovolicc2  25430  ismbl2  25435  nulmbl  25443  nulmbl2  25444  unmbl  25445  shftmbl  25446  voliunlem3  25460  volsup  25464  ioombl1lem4  25469  ioombl1  25470  icombl  25472  ioombl  25473  uniioombl  25497  opnmbllem  25509  volivth  25515  vitali  25521  mbflimsup  25574  i1fadd  25603  itg1addlem4  25607  itg2le  25647  itg2seq  25650  itg2lea  25652  itg2splitlem  25656  itg2split  25657  itg2mono  25661  itg2gt0  25668  itg2cnlem2  25670  itgss  25720  itgfsum  25735  itgcn  25753  ellimc3  25787  limcco  25801  limciun  25802  dvnres  25840  dvnfre  25863  rolle  25901  c1liplem1  25908  dvivth  25922  dvne0  25923  lhop1lem  25925  lhop1  25926  lhop  25928  dvcnvrelem1  25929  dvfsumrlim  25945  dvfsum2  25948  ftc1a  25951  ftc1lem6  25955  itgsubst  25963  tdeglem4  25972  mdegaddle  25986  mdegvscale  25987  mdegmullem  25990  deg1tmle  26030  ply1divex  26049  dvdsq1p  26075  fta1g  26082  fta1b  26084  plyco0  26104  coeeulem  26136  dgrlem  26141  plyco  26153  coemullem  26162  dgreq0  26178  dgrco  26188  plydivex  26212  quotcan  26224  aannenlem1  26243  aalioulem2  26248  aalioulem3  26249  taylthlem1  26288  ulmbdd  26314  itgulm  26324  radcnvlt1  26334  psercnlem1  26342  abelthlem2  26349  abelthlem8  26356  logcnlem5  26562  efopn  26574  cxpmul2z  26607  cxpcn3lem  26664  cxpeq  26674  xrlimcnp  26885  cxplim  26889  o1cxp  26892  cxploglim  26895  scvxcvx  26903  jensen  26906  ftalem1  26990  ftalem2  26991  fta  26997  basellem3  27000  isppw2  27032  ppinprm  27069  chtnprm  27071  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chtublem  27129  perfectlem2  27148  dchrfi  27173  dchrptlem1  27182  dchrptlem2  27183  dchrptlem3  27184  dchrsum2  27186  bposlem1  27202  bposlem3  27204  2sqlem5  27340  2sqlem6  27341  2sqlem8  27344  2sqlem10  27346  2sqb  27350  chebbnd1lem1  27387  chtppilimlem2  27392  dchrisum0flb  27428  dchrisum0fno1  27429  dchrisum0  27438  pntrsumbnd2  27485  pntpbnd1  27504  pntpbnd2  27505  pntlemp  27528  pnt3  27530  qabvle  27543  ostth2lem2  27552  ostth3  27556  ostth  27557  nolt02o  27614  nogt01o  27615  nosupprefixmo  27619  noinfprefixmo  27620  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noetasuplem4  27655  noetainflem4  27659  etasslt  27732  cuteq1  27753  madebdaylemlrcut  27817  cutlt  27847  mulsuniflem  28059  bdayon  28180  om2noseqlt  28200  n0sfincut  28253  zs12ge0  28349  readdscl  28357  remulscl  28360  colinearalglem4  28843  axcontlem10  28907  upgrex  29026  smcnlem  30633  ubthlem1  30806  ubthlem3  30808  htthlem  30853  5oalem6  31595  leopmuli  32069  pjnormssi  32104  pjclem4  32135  pj3si  32143  hatomistici  32298  sumdmdlem  32354  sgn3da  32767  wrdt2ind  32883  xrge0tsmsd  33010  isarchiofld  33303  ordtrest2NEWlem  33920  qqhf  33984  eulerpartlemb  34367  ballotlemfc0  34492  ballotlemfcc  34493  subfacp1lem5  35173  erdszelem7  35186  erdszelem11  35190  pconnconn  35220  txpconn  35221  connpconn  35224  sconnpi1  35228  txsconn  35230  cvxsconn  35232  cvmopnlem  35267  cvmfolem  35268  cvmliftmolem2  35271  cvmliftlem7  35280  cvmliftlem10  35283  cvmlift2lem10  35301  cvmlift3lem4  35311  cvmlift3lem8  35315  satfun  35400  msubff1  35545  wzel  35809  wsuclem  35810  btwnouttr2  36007  cgrxfr  36040  btwnxfr  36041  brcolinear  36044  lineext  36061  btwnconn1lem13  36084  midofsegid  36089  segcon2  36090  brsegle  36093  seglecgr12im  36095  segletr  36099  colinbtwnle  36103  broutsideof2  36107  btwnoutside  36110  broutsideof3  36111  outsideoftr  36114  outsideofeq  36115  outsideofeu  36116  outsidele  36117  lineunray  36132  lineelsb2  36133  linethru  36138  finminlem  36303  nn0prpwlem  36307  neibastop2lem  36345  neibastop2  36346  neibastop3  36347  topjoin  36350  tailfb  36362  relowlssretop  37348  fvineqsneq  37397  wl-sbcom2d-lem1  37544  finixpnum  37596  poimirlem6  37617  poimirlem7  37618  poimirlem13  37624  poimirlem26  37637  poimirlem29  37640  heicant  37646  opnmbllem0  37647  mblfinlem3  37650  ismblfin  37652  ovoliunnfl  37653  voliunnfl  37655  volsupnfl  37656  itg2addnclem  37662  itg2addnclem3  37664  ftc1cnnc  37683  sdclem2  37733  fdc  37736  istotbnd3  37762  isbnd2  37774  isbnd3  37775  prdsbnd  37784  cntotbnd  37787  heibor1lem  37800  heibor1  37801  heiborlem10  37811  rrncmslem  37823  ghomco  37882  1idl  38017  unichnidl  38022  disjlem18  38785  prtlem10  38850  prtlem18  38862  atlatmstc  39304  cvrexchlem  39405  paddasslem14  39819  pexmidlem5N  39960  cdleme29ex  40360  cdlemefr29exN  40388  cdleme32fva  40423  diarnN  41115  dihlsscpre  41220  isnacs3  42670  fnwe2lem2  43012  kelac1  43024  hbtlem5  43089  hbt  43091  dgraa0p  43110  ofoafg  43315  ofoafo  43317  naddcnffo  43325  fzunt  43416  fzuntd  43417  monoordxrv  45450  rlimdmafv  47148  rlimdmafv2  47229  fmtnoprmfac2  47523  perfectALTVlem2  47678  mogoldbb  47741  lindslinindsimp2  48381