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  5100  wereu2  5652  frpomin  6338  ordtr3  6404  fcof1  7289  knatar  7361  riota5f  7399  ovmpodf  7570  extmptsuppeq  8187  suppss  8193  suppss2  8199  frrlem14  8299  fprresex  8310  smoord  8355  tfrlem9a  8376  oaass  8551  oelimcl  8591  oaabs2  8640  cofon1  8663  naddssim  8677  swoso  8734  eceqoveq  8825  domdifsn  9061  domunsncan  9078  omxpenlem  9079  enfixsn  9087  mapdom2  9149  frfi  9258  fofinf1o  9302  finsschain  9329  elfiun  9403  marypha1lem  9406  eqsupd  9430  eqinfd  9459  ordiso2  9490  ordtypelem6  9498  ordtypelem7  9499  ordtypelem10  9502  oismo  9515  wemapsolem  9525  brwdom2  9548  wdomtr  9550  unwdomg  9559  xpwdomg  9560  unxpwdom2  9563  cantnfval2  9651  cantnfle  9653  cantnflem1  9671  cantnf  9675  r1ordg  9763  tcrank  9869  carddomi2  9978  harval2  10005  infxpenlem  10019  infxpenc2lem2  10026  fseqenlem1  10030  dfac8clem  10038  acndom2  10060  infpwfien  10068  iunfictbso  10120  dfac12lem3  10151  infxp  10219  coflim  10266  cofsmo  10274  coftr  10278  sornom  10282  infpssrlem4  10311  enfin2i  10326  fin23lem26  10330  fin23lem27  10333  fin23lem36  10353  fin23lem40  10356  isf32lem5  10362  isf34lem4  10382  isfin1-3  10391  fin1a2lem10  10414  fin1a2lem13  10417  fin1a2s  10419  hsmexlem4  10434  ttukeylem5  10518  ttukeylem6  10519  ttukeylem7  10520  alephval2  10584  gchor  10639  fpwwe2lem6  10648  fpwwe2lem11  10653  fpwwe2  10655  pwfseqlem4a  10673  pwfseqlem4  10674  winalim2  10708  gchina  10711  inar1  10787  nqereq  10947  prlem934  11045  prlem936  11059  addsrmo  11085  mulsrmo  11086  supsrlem  11123  axpre-sup  11181  dedekind  11400  dedekindle  11401  mulge0b  12112  supaddc  12209  supmul1  12211  un0addcl  12564  un0mulcl  12565  uzwo3  12995  qbtwnre  13254  xlemul1a  13343  seqcl2  14087  seqfveq2  14091  seqshft2  14095  monoord  14099  seqsplit  14102  seqf1olem1  14108  seqid2  14115  seqhomo  14116  expnegz  14163  expcan  14236  ltexp2  14237  discr  14307  bcval5  14385  hashbc  14521  hashf1lem2  14524  seqcoll  14532  seqcoll2  14533  wrdind  14794  wrd2ind  14795  sgn3da  15177  cau3lem  15445  ello1d  15613  lo1bdd2  15614  rlimclim  15636  climrlim2  15637  rlimdm  15641  rlimcn1  15678  reccn2  15687  rlimsqzlem  15739  lo1le  15742  caucvgrlem  15763  caurcvg2  15768  summolem2  15805  zsum  15807  fsum  15809  fsumf1o  15812  sumss  15813  fsumss  15814  fsumcl2lem  15820  fsumadd  15829  fsumcom2  15863  fsum0diag2  15872  fsummulc2  15873  fsumconst  15879  fsumrelem  15897  fsumrlim  15901  fsumo1  15902  divrcnv  15944  geomulcvg  15968  mertenslem2  15977  prodmolem2  16025  zprod  16027  fprod  16031  fprodf1o  16036  prodss  16037  fprodss  16038  fprodcl2lem  16040  fprodmul  16050  fproddiv  16051  fprodconst  16068  fprodn0  16069  fprodcom2  16074  ruclem8  16328  dvds0lem  16359  dvdsnegb  16366  dvdssub2  16394  bitsf1  16539  bitsshft  16568  bezoutlem3  16634  bezoutlem4  16635  isprm5  16801  isprm6  16808  hashgcdeq  16884  modprminv  16894  modprminveq  16895  reumodprminv  16899  pcqmul  16948  pcqcl  16951  pcxnn0cl  16955  pcxcl  16956  pc2dvds  16974  pcadd  16984  pcmpt  16987  pockthg  17001  infpnlem1  17005  prmreclem5  17015  vdwlem2  17077  vdwlem9  17084  vdwlem10  17085  vdwlem12  17087  ramub  17108  0ram  17115  ramub1lem2  17122  ramub1  17123  ramcl  17124  mreexexd  17739  acsfn2  17754  iscatd  17764  catpropd  17800  setcmon  18179  pleval2i  18425  psss  18671  mgmidsssn0  18769  mgmhmeql  18821  mhmeql  18938  frmdss2  18975  frmdup3  18979  grprcan  19100  dfgrp3lem  19164  mulgnn0ass  19236  isnsg3  19286  ghmpreima  19368  ghmeql  19369  gaorber  19438  f1omvdco2  19578  psgnunilem1  19623  psgnunilem2  19625  oddvds  19677  gexdvds  19714  sylow1lem1  19728  odcau  19734  pgpssslw  19744  sylow2alem2  19748  sylow2blem3  19752  fislw  19755  lsmmod  19805  efgredlem  19877  frgpup3  19908  gsumval3  20037  gsumzres  20039  gsumzcl2  20040  gsumzf1o  20042  gsumzaddlem  20051  gsumconst  20064  gsumzmhm  20067  gsumzoppg  20074  gsum2d2lem  20103  ablfac1eulem  20204  pgpfac1lem5  20211  ablfaclem3  20219  issubdrg  20949  lss1d  21150  lmhmeql  21242  lspextmo  21243  lspsnat  21335  lsppratlem6  21342  islbs3  21345  lbsextlem4  21351  lidl1el  21417  cnsubrg  21643  gsumfsum  21650  prmirredlem  21688  znidomb  21777  frgpcyg  21789  cssmre  21909  dsmmsubg  21959  dsmmlss  21960  frlmsslsp  22012  lindff1  22036  lindfrn  22037  rnasclassa  22113  mvrf1  22203  mplsubglem  22216  mpllsslem  22217  mplcoe1  22256  mplcoe5  22259  gsummoncoe1  22536  mat1dimcrng  22702  mdetdiaglem  22823  mdetunilem7  22843  mdetunilem8  22844  mdetunilem9  22845  cpmatacl  22944  cpmatmcllem  22946  mp2pm2mplem4  23037  en2top  23213  toponmre  23321  topssnei  23352  innei  23353  clslp  23376  restcls  23409  restntr  23410  ordtrest2lem  23431  cnpco  23495  cncls2  23501  cncnpi  23506  cncnp  23508  cnconst2  23511  cnpdis  23521  lmcnp  23532  cnhaus  23582  isreg2  23605  cncmp  23620  tgcmp  23629  sscmp  23633  cmpfi  23636  cnconn  23650  iunconnlem  23655  clsconn  23658  1stcfb  23673  1stcrest  23681  2ndcctbss  23684  2ndcdisj  23685  1stcelcls  23690  1stccnp  23691  restnlly  23711  cldllycmp  23724  lly1stc  23725  dislly  23726  locfincmp  23755  comppfsc  23761  kgentopon  23767  kgenidm  23776  1stckgenlem  23782  kgencn3  23787  ptpjpre1  23800  ptbasin  23806  txcls  23833  tx2cn  23839  ptpjcn  23840  ptclsg  23844  ptcnp  23851  txdis  23861  txlly  23865  txnlly  23866  pthaus  23867  txtube  23869  txcmplem1  23870  txcmplem2  23871  txcmp  23872  txhaus  23876  txkgen  23881  xkohaus  23882  xkococnlem  23888  xkococn  23889  txconn  23918  qtopeu  23945  qtoprest  23946  regr1lem2  23969  kqreglem1  23970  cmphaushmeo  24029  xkocnv  24043  fgabs  24108  filuni  24114  trufil  24139  ufileu  24148  filufint  24149  fin1aufil  24161  elfm2  24177  rnelfmlem  24181  fmfnfmlem2  24184  fmfnfmlem4  24186  fmufil  24188  flimopn  24204  fbflim2  24206  hausflimi  24209  hausflim  24210  flimcf  24211  flimclslem  24213  flimsncls  24215  hauspwpwf1  24216  cnpflfi  24228  fclsnei  24248  fclscf  24254  flimfnfcls  24257  fclscmp  24259  ufilcmp  24261  fcfnei  24264  cnpfcf  24270  alexsublem  24273  alexsub  24274  alexsubALTlem2  24277  alexsubALTlem3  24278  alexsubALTlem4  24279  ptcmplem3  24283  ptcmplem4  24284  ptcmplem5  24285  symgtgp  24335  tgpconncompeqg  24341  tgpconncomp  24342  ghmcnp  24344  tgpt0  24348  qustgplem  24350  haustsms2  24366  tsmsgsum  24368  tsmsres  24373  tsmsxp  24384  imasdsf1olem  24602  xbln0  24643  blssps  24653  blss  24654  neibl  24730  blcld  24734  metss  24737  metequiv2  24739  met1stc  24750  metrest  24753  prdsxmslem2  24758  metcnp3  24769  nrmmetd  24803  nlmvscnlem1  24915  nrginvrcnlem  24920  nmoleub  24960  icccmplem2  25053  icccmp  25055  reconnlem2  25057  xrge0tsms  25064  metdstri  25081  metdseq0  25084  metdscn  25086  cnmpopc  25159  lebnumlem3  25194  pcoval2  25247  pcopt  25253  nmoleub2lem  25345  nmhmcn  25351  ipcnlem1  25476  cfilfcls  25505  cmetcaulem  25519  iscmet3lem2  25523  iscmet3  25524  equivcau  25531  caubl  25539  bcthlem2  25556  bcthlem3  25557  bcthlem4  25558  bcthlem5  25559  ivthlem2  25683  ivthlem3  25684  ovoliunlem2  25734  ovolicc2lem2  25749  ovolicc2lem5  25752  ovolicc2  25753  ismbl2  25758  nulmbl  25766  nulmbl2  25767  unmbl  25768  shftmbl  25769  voliunlem3  25783  volsup  25787  ioombl1lem4  25792  ioombl1  25793  icombl  25795  ioombl  25796  uniioombl  25820  opnmbllem  25832  volivth  25838  vitali  25844  mbflimsup  25897  i1fadd  25926  itg1addlem4  25930  itg2le  25970  itg2seq  25973  itg2lea  25975  itg2splitlem  25979  itg2split  25980  itg2mono  25984  itg2gt0  25991  itg2cnlem2  25993  itgss  26042  itgfsum  26057  itgcn  26075  ellimc3  26109  limcco  26123  limciun  26124  dvnres  26161  dvnfre  26182  rolle  26220  c1liplem1  26226  dvivth  26240  dvne0  26241  lhop1lem  26243  lhop1  26244  lhop  26246  dvcnvrelem1  26247  dvfsumrlim  26261  dvfsum2  26264  ftc1a  26267  ftc1lem6  26271  itgsubst  26279  tdeglem4  26288  mdegaddle  26302  mdegvscale  26303  mdegmullem  26306  deg1tmle  26346  ply1divex  26365  dvdsq1p  26391  fta1g  26398  fta1b  26400  plyco0  26420  coeeulem  26453  dgrlem  26458  plyco  26470  coemullem  26479  dgreq0  26494  dgrco  26504  plydivex  26530  quotcan  26544  aannenlem1  26567  aalioulem2  26572  aalioulem3  26573  taylthlem1  26612  ulmbdd  26637  itgulm  26647  radcnvlt1  26657  psercnlem1  26664  abelthlem2  26671  abelthlem8  26678  logcnlem5  26886  efopn  26898  cxpmul2z  26931  cxpcn3lem  26987  cxpeq  26997  xrlimcnp  27208  cxplim  27211  o1cxp  27214  cxploglim  27217  scvxcvx  27225  jensen  27228  ftalem1  27312  ftalem2  27313  fta  27319  basellem3  27322  isppw2  27354  ppinprm  27391  chtnprm  27393  mpodvdsmulf1o  27433  dvdsmulf1o  27435  chtublem  27450  perfectlem2  27469  dchrfi  27494  dchrptlem1  27503  dchrptlem2  27504  dchrptlem3  27505  dchrsum2  27507  bposlem1  27523  bposlem3  27525  2sqlem5  27661  2sqlem6  27662  2sqlem8  27665  2sqlem10  27667  2sqb  27671  chebbnd1lem1  27708  chtppilimlem2  27713  dchrisum0flb  27749  dchrisum0fno1  27750  dchrisum0  27759  pntrsumbnd2  27806  pntpbnd1  27825  pntpbnd2  27826  pntlemp  27849  pnt3  27851  qabvle  27864  ostth2lem2  27873  ostth3  27877  ostth  27878  nolt02o  27934  nogt01o  27935  nosupprefixmo  27939  noinfprefixmo  27940  nosupbnd1lem3  27949  nosupbnd1lem4  27950  nosupbnd1lem5  27951  noinfbnd1lem3  27964  noinfbnd1lem4  27965  noinfbnd1lem5  27966  noetasuplem4  27975  noetainflem4  27979  etaslts  28061  cuteq1  28085  madebdaylemlrcut  28167  cutlt  28200  mulsuniflem  28417  bdayons  28544  addonbday  28547  om2noseqlt  28567  n0fincut  28623  bdaypw2n0bndlem  28731  bdayfinbndlem1  28735  z12sge0  28751  readdscl  28767  remulscl  28770  colinearalglem4  29369  axcontlem10  29433  upgrex  29552  smcnlem  31181  ubthlem1  31354  ubthlem3  31356  htthlem  31401  5oalem6  32143  leopmuli  32617  pjnormssi  32652  pjclem4  32683  pj3si  32691  hatomistici  32846  sumdmdlem  32902  wrdt2ind  33398  xrge0tsmsd  33516  isarchiofld  33642  ordtrest2NEWlem  34435  qqhf  34499  eulerpartlemb  34882  ballotlemfc0  35007  ballotlemfcc  35008  subfacp1lem5  35766  erdszelem7  35779  erdszelem11  35783  pconnconn  35813  txpconn  35814  connpconn  35817  sconnpi1  35821  txsconn  35823  cvxsconn  35825  cvmopnlem  35860  cvmfolem  35861  cvmliftmolem2  35864  cvmliftlem7  35873  cvmliftlem10  35876  cvmlift2lem10  35894  cvmlift3lem4  35904  cvmlift3lem8  35908  satfun  35993  msubff1  36138  wzel  36404  wsuclem  36405  btwnouttr2  36605  cgrxfr  36638  btwnxfr  36639  brcolinear  36642  lineext  36659  btwnconn1lem13  36682  midofsegid  36687  segcon2  36688  brsegle  36691  seglecgr12im  36693  segletr  36697  colinbtwnle  36701  broutsideof2  36705  btwnoutside  36708  broutsideof3  36709  outsideoftr  36712  outsideofeq  36713  outsideofeu  36714  outsidele  36715  lineunray  36730  lineelsb2  36731  linethru  36736  nmulrid  36780  nmuladdss  36796  nadddilem1  36803  finminlem  36940  nn0prpwlem  36944  neibastop2lem  36982  neibastop2  36983  neibastop3  36984  topjoin  36987  tailfb  36999  axtcond  37100  relowlssretop  38120  fvineqsneq  38169  wl-sbcom2d-lem1  38325  finixpnum  38362  poimirlem6  38378  poimirlem7  38379  poimirlem13  38385  poimirlem26  38398  poimirlem29  38401  heicant  38407  opnmbllem0  38408  mblfinlem3  38411  ismblfin  38413  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  itg2addnclem  38423  itg2addnclem3  38425  ftc1cnnc  38444  sdclem2  38495  fdc  38498  istotbnd3  38524  isbnd2  38536  isbnd3  38537  prdsbnd  38546  cntotbnd  38549  heibor1lem  38562  heibor1  38563  heiborlem10  38573  rrncmslem  38585  ghomco  38644  1idl  38779  unichnidl  38784  disjlem18  39654  prtlem10  39741  prtlem18  39753  atlatmstc  40195  cvrexchlem  40295  paddasslem14  40709  pexmidlem5N  40850  cdleme29ex  41250  cdlemefr29exN  41278  cdleme32fva  41313  diarnN  42005  dihlsscpre  42110  isnacs3  43558  fnwe2lem2  43895  kelac1  43907  hbtlem5  43972  hbt  43974  dgraa0p  43993  ofoafg  44198  ofoafo  44200  naddcnffo  44208  fzunt  44298  fzuntd  44299  monoordxrv  46312  rlimdmafv  48068  rlimdmafv2  48149  fmtnoprmfac2  48473  perfectALTVlem2  48641  mogoldbb  48704  lindslinindsimp2  49396