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  3131  reximddv  3145  disjxiun  5089  wereu2  5616  frpomin  6288  ordtr3  6353  fcof1  7224  knatar  7294  riota5f  7334  ovmpodf  7505  extmptsuppeq  8121  suppss  8127  suppss2  8133  frrlem14  8232  fprresex  8243  smoord  8288  tfrlem9a  8308  oaass  8479  oelimcl  8518  oaabs2  8567  cofon1  8590  naddssim  8603  swoso  8659  eceqoveq  8749  domdifsn  8977  domunsncan  8994  omxpenlem  8995  enfixsn  9003  mapdom2  9065  frfi  9174  fofinf1o  9222  finsschain  9249  elfiun  9320  marypha1lem  9323  eqsupd  9347  eqinfd  9376  ordiso2  9407  ordtypelem6  9415  ordtypelem7  9416  ordtypelem10  9419  oismo  9432  wemapsolem  9442  brwdom2  9465  wdomtr  9467  unwdomg  9476  xpwdomg  9477  unxpwdom2  9480  cantnfval2  9565  cantnfle  9567  cantnflem1  9585  cantnf  9589  r1ordg  9674  tcrank  9780  carddomi2  9866  harval2  9893  infxpenlem  9907  infxpenc2lem2  9914  fseqenlem1  9918  dfac8clem  9926  acndom2  9948  infpwfien  9956  iunfictbso  10008  dfac12lem3  10040  infxp  10108  coflim  10155  cofsmo  10163  coftr  10167  sornom  10171  infpssrlem4  10200  enfin2i  10215  fin23lem26  10219  fin23lem27  10222  fin23lem36  10242  fin23lem40  10245  isf32lem5  10251  isf34lem4  10271  isfin1-3  10280  fin1a2lem10  10303  fin1a2lem13  10306  fin1a2s  10308  hsmexlem4  10323  ttukeylem5  10407  ttukeylem6  10408  ttukeylem7  10409  alephval2  10466  gchor  10521  fpwwe2lem6  10530  fpwwe2lem11  10535  fpwwe2  10537  pwfseqlem4a  10555  pwfseqlem4  10556  winalim2  10590  gchina  10593  inar1  10669  nqereq  10829  prlem934  10927  prlem936  10941  addsrmo  10967  mulsrmo  10968  supsrlem  11005  axpre-sup  11063  dedekind  11279  dedekindle  11280  mulge0b  11995  supaddc  12092  supmul1  12094  un0addcl  12417  un0mulcl  12418  uzwo3  12844  qbtwnre  13101  xlemul1a  13190  seqcl2  13927  seqfveq2  13931  seqshft2  13935  monoord  13939  seqsplit  13942  seqf1olem1  13948  seqid2  13955  seqhomo  13956  expnegz  14003  expcan  14076  ltexp2  14077  discr  14147  bcval5  14225  hashbc  14360  hashf1lem2  14363  seqcoll  14371  seqcoll2  14372  wrdind  14628  wrd2ind  14629  cau3lem  15262  ello1d  15430  lo1bdd2  15431  rlimclim  15453  climrlim2  15454  rlimdm  15458  rlimcn1  15495  reccn2  15504  rlimsqzlem  15556  lo1le  15559  caucvgrlem  15580  caurcvg2  15585  summolem2  15623  zsum  15625  fsum  15627  fsumf1o  15630  sumss  15631  fsumss  15632  fsumcl2lem  15638  fsumadd  15647  fsumcom2  15681  fsum0diag2  15690  fsummulc2  15691  fsumconst  15697  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  divrcnv  15759  geomulcvg  15783  mertenslem2  15792  prodmolem2  15842  zprod  15844  fprod  15848  fprodf1o  15853  prodss  15854  fprodss  15855  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodconst  15885  fprodn0  15886  fprodcom2  15891  ruclem8  16146  dvds0lem  16177  dvdsnegb  16184  dvdssub2  16212  bitsf1  16357  bitsshft  16386  bezoutlem3  16452  bezoutlem4  16453  isprm5  16618  isprm6  16625  hashgcdeq  16701  modprminv  16711  modprminveq  16712  reumodprminv  16716  pcqmul  16765  pcqcl  16768  pcxnn0cl  16772  pcxcl  16773  pc2dvds  16791  pcadd  16801  pcmpt  16804  pockthg  16818  infpnlem1  16822  prmreclem5  16832  vdwlem2  16894  vdwlem9  16901  vdwlem10  16902  vdwlem12  16904  ramub  16925  0ram  16932  ramub1lem2  16939  ramub1  16940  ramcl  16941  mreexexd  17554  acsfn2  17569  iscatd  17579  catpropd  17615  setcmon  17994  pleval2i  18240  psss  18486  mgmidsssn0  18546  mgmhmeql  18590  mhmeql  18700  frmdss2  18737  frmdup3  18741  grprcan  18852  dfgrp3lem  18917  mulgnn0ass  18989  isnsg3  19039  ghmpreima  19117  ghmeql  19118  gaorber  19187  f1omvdco2  19327  psgnunilem1  19372  psgnunilem2  19374  oddvds  19426  gexdvds  19463  sylow1lem1  19477  odcau  19483  pgpssslw  19493  sylow2alem2  19497  sylow2blem3  19501  fislw  19504  lsmmod  19554  efgredlem  19626  frgpup3  19657  gsumval3  19786  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  gsum2d2lem  19852  ablfac1eulem  19953  pgpfac1lem5  19960  ablfaclem3  19968  issubdrg  20665  lss1d  20866  lmhmeql  20959  lspextmo  20960  lspsnat  21052  lsppratlem6  21059  islbs3  21062  lbsextlem4  21068  lidl1el  21133  cnsubrg  21334  gsumfsum  21341  prmirredlem  21379  znidomb  21468  frgpcyg  21480  cssmre  21600  dsmmsubg  21650  dsmmlss  21651  frlmsslsp  21703  lindff1  21727  lindfrn  21728  rnasclassa  21802  mvrf1  21893  mplsubglem  21906  mpllsslem  21907  mplcoe1  21942  mplcoe5  21945  gsummoncoe1  22193  mat1dimcrng  22362  mdetdiaglem  22483  mdetunilem7  22503  mdetunilem8  22504  mdetunilem9  22505  cpmatacl  22601  cpmatmcllem  22603  mp2pm2mplem4  22694  en2top  22870  toponmre  22978  topssnei  23009  innei  23010  clslp  23033  restcls  23066  restntr  23067  ordtrest2lem  23088  cnpco  23152  cncls2  23158  cncnpi  23163  cncnp  23165  cnconst2  23168  cnpdis  23178  lmcnp  23189  cnhaus  23239  isreg2  23262  cncmp  23277  tgcmp  23286  sscmp  23290  cmpfi  23293  cnconn  23307  iunconnlem  23312  clsconn  23315  1stcfb  23330  1stcrest  23338  2ndcctbss  23340  2ndcdisj  23341  1stcelcls  23346  1stccnp  23347  restnlly  23367  cldllycmp  23380  lly1stc  23381  dislly  23382  locfincmp  23411  comppfsc  23417  kgentopon  23423  kgenidm  23432  1stckgenlem  23438  kgencn3  23443  ptpjpre1  23456  ptbasin  23462  txcls  23489  tx2cn  23495  ptpjcn  23496  ptclsg  23500  ptcnp  23507  txdis  23517  txlly  23521  txnlly  23522  pthaus  23523  txtube  23525  txcmplem1  23526  txcmplem2  23527  txcmp  23528  txhaus  23532  txkgen  23537  xkohaus  23538  xkococnlem  23544  xkococn  23545  txconn  23574  qtopeu  23601  qtoprest  23602  regr1lem2  23625  kqreglem1  23626  cmphaushmeo  23685  xkocnv  23699  fgabs  23764  filuni  23770  trufil  23795  ufileu  23804  filufint  23805  fin1aufil  23817  elfm2  23833  rnelfmlem  23837  fmfnfmlem2  23840  fmfnfmlem4  23842  fmufil  23844  flimopn  23860  fbflim2  23862  hausflimi  23865  hausflim  23866  flimcf  23867  flimclslem  23869  flimsncls  23871  hauspwpwf1  23872  cnpflfi  23884  fclsnei  23904  fclscf  23910  flimfnfcls  23913  fclscmp  23915  ufilcmp  23917  fcfnei  23920  cnpfcf  23926  alexsublem  23929  alexsub  23930  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  ptcmplem3  23939  ptcmplem4  23940  ptcmplem5  23941  symgtgp  23991  tgpconncompeqg  23997  tgpconncomp  23998  ghmcnp  24000  tgpt0  24004  qustgplem  24006  haustsms2  24022  tsmsgsum  24024  tsmsres  24029  tsmsxp  24040  imasdsf1olem  24259  xbln0  24300  blssps  24310  blss  24311  neibl  24387  blcld  24391  metss  24394  metequiv2  24396  met1stc  24407  metrest  24410  prdsxmslem2  24415  metcnp3  24426  nrmmetd  24460  nlmvscnlem1  24572  nrginvrcnlem  24577  nmoleub  24617  icccmplem2  24710  icccmp  24712  reconnlem2  24714  xrge0tsms  24721  metdstri  24738  metdseq0  24741  metdscn  24743  cnmpopc  24820  lebnumlem3  24860  pcoval2  24914  pcopt  24920  nmoleub2lem  25012  nmhmcn  25018  ipcnlem1  25143  cfilfcls  25172  cmetcaulem  25186  iscmet3lem2  25190  iscmet3  25191  equivcau  25198  caubl  25206  bcthlem2  25223  bcthlem3  25224  bcthlem4  25225  bcthlem5  25226  ivthlem2  25351  ivthlem3  25352  ovoliunlem2  25402  ovolicc2lem2  25417  ovolicc2lem5  25420  ovolicc2  25421  ismbl2  25426  nulmbl  25434  nulmbl2  25435  unmbl  25436  shftmbl  25437  voliunlem3  25451  volsup  25455  ioombl1lem4  25460  ioombl1  25461  icombl  25463  ioombl  25464  uniioombl  25488  opnmbllem  25500  volivth  25506  vitali  25512  mbflimsup  25565  i1fadd  25594  itg1addlem4  25598  itg2le  25638  itg2seq  25641  itg2lea  25643  itg2splitlem  25647  itg2split  25648  itg2mono  25652  itg2gt0  25659  itg2cnlem2  25661  itgss  25711  itgfsum  25726  itgcn  25744  ellimc3  25778  limcco  25792  limciun  25793  dvnres  25831  dvnfre  25854  rolle  25892  c1liplem1  25899  dvivth  25913  dvne0  25914  lhop1lem  25916  lhop1  25917  lhop  25919  dvcnvrelem1  25920  dvfsumrlim  25936  dvfsum2  25939  ftc1a  25942  ftc1lem6  25946  itgsubst  25954  tdeglem4  25963  mdegaddle  25977  mdegvscale  25978  mdegmullem  25981  deg1tmle  26021  ply1divex  26040  dvdsq1p  26066  fta1g  26073  fta1b  26075  plyco0  26095  coeeulem  26127  dgrlem  26132  plyco  26144  coemullem  26153  dgreq0  26169  dgrco  26179  plydivex  26203  quotcan  26215  aannenlem1  26234  aalioulem2  26239  aalioulem3  26240  taylthlem1  26279  ulmbdd  26305  itgulm  26315  radcnvlt1  26325  psercnlem1  26333  abelthlem2  26340  abelthlem8  26347  logcnlem5  26553  efopn  26565  cxpmul2z  26598  cxpcn3lem  26655  cxpeq  26665  xrlimcnp  26876  cxplim  26880  o1cxp  26883  cxploglim  26886  scvxcvx  26894  jensen  26897  ftalem1  26981  ftalem2  26982  fta  26988  basellem3  26991  isppw2  27023  ppinprm  27060  chtnprm  27062  mpodvdsmulf1o  27102  dvdsmulf1o  27104  chtublem  27120  perfectlem2  27139  dchrfi  27164  dchrptlem1  27173  dchrptlem2  27174  dchrptlem3  27175  dchrsum2  27177  bposlem1  27193  bposlem3  27195  2sqlem5  27331  2sqlem6  27332  2sqlem8  27335  2sqlem10  27337  2sqb  27341  chebbnd1lem1  27378  chtppilimlem2  27383  dchrisum0flb  27419  dchrisum0fno1  27420  dchrisum0  27429  pntrsumbnd2  27476  pntpbnd1  27495  pntpbnd2  27496  pntlemp  27519  pnt3  27521  qabvle  27534  ostth2lem2  27543  ostth3  27547  ostth  27548  nolt02o  27605  nogt01o  27606  nosupprefixmo  27610  noinfprefixmo  27611  nosupbnd1lem3  27620  nosupbnd1lem4  27621  nosupbnd1lem5  27622  noinfbnd1lem3  27635  noinfbnd1lem4  27636  noinfbnd1lem5  27637  noetasuplem4  27646  noetainflem4  27650  etasslt  27724  cuteq1  27748  madebdaylemlrcut  27813  cutlt  27845  mulsuniflem  28057  bdayon  28178  om2noseqlt  28198  n0sfincut  28251  zs12ge0  28360  readdscl  28368  remulscl  28371  colinearalglem4  28854  axcontlem10  28918  upgrex  29037  smcnlem  30641  ubthlem1  30814  ubthlem3  30816  htthlem  30861  5oalem6  31603  leopmuli  32077  pjnormssi  32112  pjclem4  32143  pj3si  32151  hatomistici  32306  sumdmdlem  32362  sgn3da  32780  wrdt2ind  32896  xrge0tsmsd  33016  isarchiofld  33142  ordtrest2NEWlem  33895  qqhf  33959  eulerpartlemb  34342  ballotlemfc0  34467  ballotlemfcc  34468  subfacp1lem5  35167  erdszelem7  35180  erdszelem11  35184  pconnconn  35214  txpconn  35215  connpconn  35218  sconnpi1  35222  txsconn  35224  cvxsconn  35226  cvmopnlem  35261  cvmfolem  35262  cvmliftmolem2  35265  cvmliftlem7  35274  cvmliftlem10  35277  cvmlift2lem10  35295  cvmlift3lem4  35305  cvmlift3lem8  35309  satfun  35394  msubff1  35539  wzel  35808  wsuclem  35809  btwnouttr2  36006  cgrxfr  36039  btwnxfr  36040  brcolinear  36043  lineext  36060  btwnconn1lem13  36083  midofsegid  36088  segcon2  36089  brsegle  36092  seglecgr12im  36094  segletr  36098  colinbtwnle  36102  broutsideof2  36106  btwnoutside  36109  broutsideof3  36110  outsideoftr  36113  outsideofeq  36114  outsideofeu  36115  outsidele  36116  lineunray  36131  lineelsb2  36132  linethru  36137  finminlem  36302  nn0prpwlem  36306  neibastop2lem  36344  neibastop2  36345  neibastop3  36346  topjoin  36349  tailfb  36361  relowlssretop  37347  fvineqsneq  37396  wl-sbcom2d-lem1  37543  finixpnum  37595  poimirlem6  37616  poimirlem7  37617  poimirlem13  37623  poimirlem26  37636  poimirlem29  37639  heicant  37645  opnmbllem0  37646  mblfinlem3  37649  ismblfin  37651  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  itg2addnclem  37661  itg2addnclem3  37663  ftc1cnnc  37682  sdclem2  37732  fdc  37735  istotbnd3  37761  isbnd2  37773  isbnd3  37774  prdsbnd  37783  cntotbnd  37786  heibor1lem  37799  heibor1  37800  heiborlem10  37810  rrncmslem  37822  ghomco  37881  1idl  38016  unichnidl  38021  disjlem18  38788  prtlem10  38854  prtlem18  38866  atlatmstc  39308  cvrexchlem  39408  paddasslem14  39822  pexmidlem5N  39963  cdleme29ex  40363  cdlemefr29exN  40391  cdleme32fva  40426  diarnN  41118  dihlsscpre  41223  isnacs3  42693  fnwe2lem2  43034  kelac1  43046  hbtlem5  43111  hbt  43113  dgraa0p  43132  ofoafg  43337  ofoafo  43339  naddcnffo  43347  fzunt  43438  fzuntd  43439  monoordxrv  45470  rlimdmafv  47171  rlimdmafv2  47252  fmtnoprmfac2  47561  perfectALTVlem2  47716  mogoldbb  47779  lindslinindsimp2  48458