Theorem expr 462

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  animpimp2impd  860  3expia  1139  rexlimdvaa  3164  reximddv  3178  disjxiun  5099  wereu2  5647  frpomin  6343  ordtr3  6409  fcof1  7295  knatar  7367  riota5f  7405  ovmpodf  7576  fnwe2lem3  8147  extmptsuppeq  8205  suppss  8211  suppss2  8217  frrlem14  8317  fprresex  8328  smoord  8373  tfrlem9a  8394  oaass  8569  oelimcl  8609  oaabs2  8658  cofon1  8681  naddssim  8695  swoso  8752  eceqoveq  8843  domdifsn  9079  domunsncan  9096  omxpenlem  9097  enfixsn  9105  mapdom2  9167  frfi  9276  fofinf1o  9321  finsschain  9348  elfiun  9422  marypha1lem  9425  eqsupd  9449  eqinfd  9478  ordiso2  9509  ordtypelem6  9517  ordtypelem7  9518  ordtypelem10  9521  oismo  9534  wemapsolem  9544  brwdom2  9567  wdomtr  9569  unwdomg  9578  xpwdomg  9579  unxpwdom2  9582  cantnfval2  9670  cantnfle  9672  cantnflem1  9690  cantnf  9694  r1ordg  9785  tcrank  9901  carddomi2  10051  harval2  10078  infxpenlem  10092  infxpenc2lem2  10099  fseqenlem1  10103  dfac8clem  10111  acndom2  10133  infpwfien  10141  iunfictbso  10193  dfac12lem3  10224  infxp  10292  coflim  10339  cofsmo  10347  coftr  10351  sornom  10355  infpssrlem4  10384  enfin2i  10399  fin23lem26  10403  fin23lem27  10406  fin23lem36  10426  fin23lem40  10429  isf32lem5  10435  isf34lem4  10455  isfin1-3  10464  fin1a2lem10  10487  fin1a2lem13  10490  fin1a2s  10492  hsmexlem4  10507  ttukeylem5  10591  ttukeylem6  10592  ttukeylem7  10593  alephval2  10657  gchor  10712  fpwwe2lem6  10721  fpwwe2lem11  10726  fpwwe2  10728  pwfseqlem4a  10746  pwfseqlem4  10747  winalim2  10781  gchina  10784  inar1  10860  nqereq  11020  prlem934  11118  prlem936  11132  addsrmo  11158  mulsrmo  11159  supsrlem  11196  axpre-sup  11254  dedekind  11473  dedekindle  11474  mulge0b  12187  supaddc  12284  supmul1  12286  un0addcl  12639  un0mulcl  12640  uzwo3  13070  qbtwnre  13329  xlemul1a  13418  seqcl2  14163  seqfveq2  14167  seqshft2  14171  monoord  14175  seqsplit  14178  seqf1olem1  14184  seqid2  14191  seqhomo  14192  expnegz  14239  expcan  14312  ltexp2  14313  discr  14384  bcval5  14462  hashbc  14598  hashf1lem2  14601  seqcoll  14609  seqcoll2  14610  wrdind  14871  wrd2ind  14872  sgn3da  15254  cau3lem  15522  ello1d  15690  lo1bdd2  15691  rlimclim  15713  climrlim2  15714  rlimdm  15718  rlimcn1  15755  reccn2  15764  rlimsqzlem  15816  lo1le  15819  caucvgrlem  15840  caurcvg2  15845  summolem2  15882  zsum  15884  fsum  15886  fsumf1o  15889  sumss  15890  fsumss  15891  fsumcl2lem  15897  fsumadd  15906  fsumcom2  15940  fsum0diag2  15949  fsummulc2  15950  fsumconst  15956  fsumrelem  15974  fsumrlim  15978  fsumo1  15979  divrcnv  16021  geomulcvg  16045  mertenslem2  16054  prodmolem2  16102  zprod  16104  fprod  16108  fprodf1o  16113  prodss  16114  fprodss  16115  fprodcl2lem  16117  fprodmul  16127  fproddiv  16128  fprodconst  16145  fprodn0  16146  fprodcom2  16151  ruclem8  16405  dvds0lem  16436  dvdsnegb  16443  dvdssub2  16471  bitsf1  16616  bitsshft  16645  bezoutlem3  16714  bezoutlem4  16715  isprm5  16883  isprm6  16890  hashgcdeq  16967  modprminv  16977  modprminveq  16978  reumodprminv  16982  pcqmul  17031  pcqcl  17034  pcxnn0cl  17038  pcxcl  17039  pc2dvds  17057  pcadd  17067  pcmpt  17070  pockthg  17084  infpnlem1  17088  prmreclem5  17098  vdwlem2  17160  vdwlem9  17167  vdwlem10  17168  vdwlem12  17170  ramub  17191  0ram  17198  ramub1lem2  17205  ramub1  17206  ramcl  17207  mreexexd  17822  acsfn2  17837  iscatd  17847  catpropd  17883  setcmon  18262  pleval2i  18508  psss  18754  mgmidsssn0  18853  mgmhmeql  18905  mhmeql  19022  frmdss2  19059  frmdup3  19063  grprcan  19184  dfgrp3lem  19248  mulgnn0ass  19320  isnsg3  19370  ghmpreima  19452  ghmeql  19453  gaorber  19522  f1omvdco2  19662  psgnunilem1  19707  psgnunilem2  19709  oddvds  19761  gexdvds  19798  sylow1lem1  19812  odcau  19818  pgpssslw  19828  sylow2alem2  19832  sylow2blem3  19836  fislw  19839  lsmmod  19889  efgredlem  19961  frgpup3  19992  gsumval3  20121  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  gsum2d2lem  20187  ablfac1eulem  20288  pgpfac1lem5  20295  ablfaclem3  20303  issubdrg  21037  lss1d  21238  lmhmeql  21330  lspextmo  21331  lspsnat  21423  lsppratlem6  21430  islbs3  21433  lbsextlem4  21439  lidl1el  21505  cnsubrg  21733  gsumfsum  21740  prmirredlem  21778  znidomb  21867  frgpcyg  21879  cssmre  21999  dsmmsubg  22049  dsmmlss  22050  frlmsslsp  22102  lindff1  22126  lindfrn  22127  rnasclassa  22203  mvrf1  22293  mplsubglem  22306  mpllsslem  22307  mplcoe1  22346  mplcoe5  22349  gsummoncoe1  22626  mat1dimcrng  22792  mdetdiaglem  22913  mdetunilem7  22933  mdetunilem8  22934  mdetunilem9  22935  cpmatacl  23034  cpmatmcllem  23036  mp2pm2mplem4  23127  en2top  23303  toponmre  23411  topssnei  23442  innei  23443  clslp  23466  restcls  23499  restntr  23500  ordtrest2lem  23521  cnpco  23585  cncls2  23591  cncnpi  23596  cncnp  23598  cnconst2  23601  cnpdis  23611  lmcnp  23622  cnhaus  23672  isreg2  23695  cncmp  23710  tgcmp  23719  sscmp  23723  cmpfi  23726  cnconn  23740  iunconnlem  23745  clsconn  23748  1stcfb  23763  1stcrest  23771  2ndcctbss  23774  2ndcdisj  23775  1stcelcls  23780  1stccnp  23781  restnlly  23801  cldllycmp  23814  lly1stc  23815  dislly  23816  locfincmp  23845  comppfsc  23851  kgentopon  23857  kgenidm  23866  1stckgenlem  23872  kgencn3  23877  ptpjpre1  23890  ptbasin  23896  txcls  23923  tx2cn  23929  ptpjcn  23930  ptclsg  23934  ptcnp  23941  txdis  23951  txlly  23955  txnlly  23956  pthaus  23957  txtube  23959  txcmplem1  23960  txcmplem2  23961  txcmp  23962  txhaus  23966  txkgen  23971  xkohaus  23972  xkococnlem  23978  xkococn  23979  txconn  24008  qtopeu  24035  qtoprest  24036  regr1lem2  24059  kqreglem1  24060  cmphaushmeo  24119  xkocnv  24133  fgabs  24198  filuni  24204  trufil  24229  ufileu  24238  filufint  24239  fin1aufil  24251  elfm2  24267  rnelfmlem  24271  fmfnfmlem2  24274  fmfnfmlem4  24276  fmufil  24278  flimopn  24294  fbflim2  24296  hausflimi  24299  hausflim  24300  flimcf  24301  flimclslem  24303  flimsncls  24305  hauspwpwf1  24306  cnpflfi  24318  fclsnei  24338  fclscf  24344  flimfnfcls  24347  fclscmp  24349  ufilcmp  24351  fcfnei  24354  cnpfcf  24360  alexsublem  24363  alexsub  24364  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem3  24373  ptcmplem4  24374  ptcmplem5  24375  symgtgp  24425  tgpconncompeqg  24431  tgpconncomp  24432  ghmcnp  24434  tgpt0  24438  qustgplem  24440  haustsms2  24456  tsmsgsum  24458  tsmsres  24463  tsmsxp  24474  imasdsf1olem  24692  xbln0  24733  blssps  24743  blss  24744  neibl  24820  blcld  24824  metss  24827  metequiv2  24829  met1stc  24840  metrest  24843  prdsxmslem2  24848  metcnp3  24859  nrmmetd  24893  nlmvscnlem1  25005  nrginvrcnlem  25010  nmoleub  25050  icccmplem2  25143  icccmp  25145  reconnlem2  25147  xrge0tsms  25154  metdstri  25171  metdseq0  25174  metdscn  25176  cnmpopc  25249  lebnumlem3  25284  pcoval2  25337  pcopt  25343  nmoleub2lem  25435  nmhmcn  25441  ipcnlem1  25566  cfilfcls  25595  cmetcaulem  25609  iscmet3lem2  25613  iscmet3  25614  equivcau  25621  caubl  25629  bcthlem2  25646  bcthlem3  25647  bcthlem4  25648  bcthlem5  25649  ivthlem2  25773  ivthlem3  25774  ovoliunlem2  25824  ovolicc2lem2  25839  ovolicc2lem5  25842  ovolicc2  25843  ismbl2  25848  nulmbl  25856  nulmbl2  25857  unmbl  25858  shftmbl  25859  voliunlem3  25873  volsup  25877  ioombl1lem4  25882  ioombl1  25883  icombl  25885  ioombl  25886  uniioombl  25910  opnmbllem  25922  volivth  25928  vitali  25934  mbflimsup  25987  i1fadd  26016  itg1addlem4  26020  itg2le  26060  itg2seq  26063  itg2lea  26065  itg2splitlem  26069  itg2split  26070  itg2mono  26074  itg2gt0  26081  itg2cnlem2  26083  itgss  26132  itgfsum  26147  itgcn  26165  ellimc3  26199  limcco  26213  limciun  26214  dvnres  26251  dvnfre  26272  rolle  26310  c1liplem1  26316  dvivth  26330  dvne0  26331  lhop1lem  26333  lhop1  26334  lhop  26336  dvcnvrelem1  26337  dvfsumrlim  26351  dvfsum2  26354  ftc1a  26357  ftc1lem6  26361  itgsubst  26369  tdeglem4  26378  mdegaddle  26392  mdegvscale  26393  mdegmullem  26396  deg1tmle  26436  ply1divex  26455  dvdsq1p  26481  fta1g  26488  fta1b  26490  plyco0  26510  coeeulem  26543  dgrlem  26548  plyco  26560  coemullem  26569  dgreq0  26584  dgrco  26594  plydivex  26618  quotcan  26632  aannenlem1  26655  aalioulem2  26660  aalioulem3  26661  taylthlem1  26700  ulmbdd  26725  itgulm  26735  radcnvlt1  26745  psercnlem1  26752  abelthlem2  26759  abelthlem8  26766  logcnlem5  26974  efopn  26986  cxpmul2z  27019  cxpcn3lem  27075  cxpeq  27085  xrlimcnp  27296  cxplim  27299  o1cxp  27302  cxploglim  27305  scvxcvx  27313  jensen  27316  ftalem1  27400  ftalem2  27401  fta  27407  basellem3  27410  isppw2  27442  ppinprm  27479  chtnprm  27481  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chtublem  27538  perfectlem2  27557  dchrfi  27582  dchrptlem1  27591  dchrptlem2  27592  dchrptlem3  27593  dchrsum2  27595  bposlem1  27611  bposlem3  27613  2sqlem5  27749  2sqlem6  27750  2sqlem8  27753  2sqlem10  27755  2sqb  27759  chebbnd1lem1  27796  chtppilimlem2  27801  dchrisum0flb  27837  dchrisum0fno1  27838  dchrisum0  27847  pntrsumbnd2  27894  pntpbnd1  27913  pntpbnd2  27914  pntlemp  27937  pnt3  27939  qabvle  27952  ostth2lem2  27961  ostth3  27965  ostth  27966  nolt02o  28052  nogt01o  28053  nosupprefixmo  28057  noinfprefixmo  28058  nosupbnd1lem3  28067  nosupbnd1lem4  28068  nosupbnd1lem5  28069  noinfbnd1lem3  28082  noinfbnd1lem4  28083  noinfbnd1lem5  28084  noetasuplem4  28093  noetainflem4  28097  etaslts  28179  cuteq1  28203  madebdaylemlrcut  28285  cutlt  28318  mulsuniflem  28535  bdayons  28662  addonbday  28665  om2noseqlt  28685  n0fincut  28741  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  z12sge0  28869  readdscl  28885  remulscl  28888  colinearalglem4  29487  axcontlem10  29551  upgrex  29670  smcnlem  31299  ubthlem1  31472  ubthlem3  31474  htthlem  31519  5oalem6  32261  leopmuli  32735  pjnormssi  32770  pjclem4  32801  pj3si  32809  hatomistici  32964  sumdmdlem  33020  wrdt2ind  33516  xrge0tsmsd  33634  isarchiofld  33760  ordtrest2NEWlem  34554  qqhf  34618  eulerpartlemb  35000  ballotlemfc0  35125  ballotlemfcc  35126  soinfdom  35717  subfacp1lem5  35949  erdszelem7  35962  erdszelem11  35966  pconnconn  35996  txpconn  35997  connpconn  36000  sconnpi1  36004  txsconn  36006  cvxsconn  36008  cvmopnlem  36043  cvmfolem  36044  cvmliftmolem2  36047  cvmliftlem7  36056  cvmliftlem10  36059  cvmlift2lem10  36077  cvmlift3lem4  36087  cvmlift3lem8  36091  satfun  36176  msubff1  36321  wzel  36586  wsuclem  36587  btwnouttr2  36787  cgrxfr  36820  btwnxfr  36821  brcolinear  36824  lineext  36841  btwnconn1lem13  36864  midofsegid  36869  segcon2  36870  brsegle  36873  seglecgr12im  36875  segletr  36879  colinbtwnle  36883  broutsideof2  36887  btwnoutside  36890  broutsideof3  36891  outsideoftr  36894  outsideofeq  36895  outsideofeu  36896  outsidele  36897  lineunray  36912  lineelsb2  36913  linethru  36918  nmulrid  36946  nmuladdss  36962  nadddilem1  36969  finminlem  37106  nn0prpwlem  37110  neibastop2lem  37148  neibastop2  37149  neibastop3  37150  topjoin  37153  tailfb  37165  axtcond  37266  relowlssretop  38287  fvineqsneq  38336  wl-sbcom2d-lem1  38492  finixpnum  38529  poimirlem6  38545  poimirlem7  38546  poimirlem13  38552  poimirlem26  38565  poimirlem29  38568  heicant  38574  opnmbllem0  38575  mblfinlem3  38578  ismblfin  38580  ovoliunnfl  38581  voliunnfl  38583  volsupnfl  38584  itg2addnclem  38590  itg2addnclem3  38592  ftc1cnnc  38611  sdclem2  38677  fdc  38680  istotbnd3  38706  isbnd2  38718  isbnd3  38719  prdsbnd  38728  cntotbnd  38731  heibor1lem  38744  heibor1  38745  heiborlem10  38755  rrncmslem  38767  ghomco  38826  1idl  38961  unichnidl  38966  disjlem18  39836  prtlem10  39923  prtlem18  39935  atlatmstc  40377  cvrexchlem  40477  paddasslem14  40891  pexmidlem5N  41032  cdleme29ex  41432  cdlemefr29exN  41460  cdleme32fva  41495  diarnN  42187  dihlsscpre  42292  isnacs3  43721  kelac1  44065  hbtlem5  44130  hbt  44132  dgraa0p  44151  ofoafg  44356  ofoafo  44358  naddcnffo  44366  fzunt  44456  fzuntd  44457  cocanss2  45922  monoordxrv  46491  rlimdmafv  48247  rlimdmafv2  48328  fmtnoprmfac2  48652  perfectALTVlem2  48820  mogoldbb  48883  lindslinindsimp2  49575