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  843  3expia  1120  reximddv  3205  rexlimdvaa  3215  disjxiun  5072  wereu2  5587  frpomin  6247  ordtr3  6315  fcof1  7168  knatar  7237  riota5f  7270  ovmpodf  7438  extmptsuppeq  8013  suppss  8019  suppssOLD  8020  suppss2  8025  frrlem14  8124  fprresex  8135  wfrlem17OLD  8165  smoord  8205  tfrlem9a  8226  oaass  8401  oelimcl  8440  oaabs2  8488  swoso  8540  eceqoveq  8620  domdifsn  8850  domunsncan  8868  omxpenlem  8869  enfixsn  8877  mapdom2  8944  frfi  9068  fofinf1o  9103  finsschain  9135  elfiun  9198  marypha1lem  9201  eqsupd  9225  eqinfd  9253  ordiso2  9283  ordtypelem6  9291  ordtypelem7  9292  ordtypelem10  9295  oismo  9308  wemapsolem  9318  brwdom2  9341  wdomtr  9343  unwdomg  9352  xpwdomg  9353  unxpwdom2  9356  cantnfval2  9436  cantnfle  9438  cantnflem1  9456  cantnf  9460  r1ordg  9545  tcrank  9651  carddomi2  9737  harval2  9764  infxpenlem  9778  infxpenc2lem2  9785  fseqenlem1  9789  dfac8clem  9797  acndom2  9819  infpwfien  9827  iunfictbso  9879  dfac12lem3  9910  infxp  9980  coflim  10026  cofsmo  10034  coftr  10038  sornom  10042  infpssrlem4  10071  enfin2i  10086  fin23lem26  10090  fin23lem27  10093  fin23lem36  10113  fin23lem40  10116  isf32lem5  10122  isf34lem4  10142  isfin1-3  10151  fin1a2lem10  10174  fin1a2lem13  10177  fin1a2s  10179  hsmexlem4  10194  ttukeylem5  10278  ttukeylem6  10279  ttukeylem7  10280  alephval2  10337  gchor  10392  fpwwe2lem6  10401  fpwwe2lem11  10406  fpwwe2  10408  pwfseqlem4a  10426  pwfseqlem4  10427  winalim2  10461  gchina  10464  inar1  10540  nqereq  10700  prlem934  10798  prlem936  10812  addsrmo  10838  mulsrmo  10839  supsrlem  10876  axpre-sup  10934  dedekind  11147  dedekindle  11148  mulge0b  11854  supaddc  11951  supmul1  11953  un0addcl  12275  un0mulcl  12276  uzwo3  12692  qbtwnre  12942  xlemul1a  13031  seqcl2  13750  seqfveq2  13754  seqshft2  13758  monoord  13762  seqsplit  13765  seqf1olem1  13771  seqid2  13778  seqhomo  13779  expnegz  13826  expcan  13896  ltexp2  13897  discr  13964  bcval5  14041  hashbc  14174  hashf1lem2  14179  seqcoll  14187  seqcoll2  14188  wrdind  14444  wrd2ind  14445  cau3lem  15075  ello1d  15241  lo1bdd2  15242  rlimclim  15264  climrlim2  15265  rlimdm  15269  rlimcn1  15306  reccn2  15315  rlimsqzlem  15369  lo1le  15372  caucvgrlem  15393  caurcvg2  15398  summolem2  15437  zsum  15439  fsum  15441  fsumf1o  15444  sumss  15445  fsumss  15446  fsumcl2lem  15452  fsumadd  15461  fsumcom2  15495  fsum0diag2  15504  fsummulc2  15505  fsumconst  15511  fsumrelem  15528  fsumrlim  15532  fsumo1  15533  divrcnv  15573  geomulcvg  15597  mertenslem2  15606  prodmolem2  15654  zprod  15656  fprod  15660  fprodf1o  15665  prodss  15666  fprodss  15667  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodconst  15697  fprodn0  15698  fprodcom2  15703  ruclem8  15955  dvds0lem  15985  dvdsnegb  15992  dvdssub2  16019  bitsf1  16162  bitsshft  16191  bezoutlem3  16258  bezoutlem4  16259  isprm5  16421  isprm6  16428  hashgcdeq  16499  modprminv  16509  modprminveq  16510  reumodprminv  16514  pcqmul  16563  pcqcl  16566  pcxnn0cl  16570  pcxcl  16571  pc2dvds  16589  pcadd  16599  pcmpt  16602  pockthg  16616  infpnlem1  16620  prmreclem5  16630  vdwlem2  16692  vdwlem9  16699  vdwlem10  16700  vdwlem12  16702  ramub  16723  0ram  16730  ramub1lem2  16737  ramub1  16738  ramcl  16739  mreexexd  17366  acsfn2  17381  iscatd  17391  catpropd  17427  setcmon  17811  pleval2i  18063  psss  18307  mgmidsssn0  18365  mhmeql  18473  frmdss2  18511  frmdup3  18515  grprcan  18622  dfgrp3lem  18682  mulgnn0ass  18748  isnsg3  18797  ghmpreima  18865  ghmeql  18866  gaorber  18923  f1omvdco2  19065  psgnunilem1  19110  psgnunilem2  19112  oddvds  19164  gexdvds  19198  sylow1lem1  19212  odcau  19218  pgpssslw  19228  sylow2alem2  19232  sylow2blem3  19236  fislw  19239  lsmmod  19290  efgredlem  19362  frgpup3  19393  gsumval3  19517  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  gsum2d2lem  19583  ablfac1eulem  19684  pgpfac1lem5  19691  ablfaclem3  19699  issubdrg  20058  lss1d  20234  lmhmeql  20326  lspextmo  20327  lspsnat  20416  lsppratlem6  20423  islbs3  20426  lbsextlem4  20432  lidl1el  20498  cnsubrg  20667  gsumfsum  20674  prmirredlem  20703  znidomb  20778  frgpcyg  20790  cssmre  20907  dsmmsubg  20959  dsmmlss  20960  frlmsslsp  21012  lindff1  21036  lindfrn  21037  rnasclassa  21108  mvrf1  21203  mplsubglem  21214  mpllsslem  21215  mplcoe1  21247  mplcoe5  21250  gsummoncoe1  21484  mat1dimcrng  21635  mdetdiaglem  21756  mdetunilem7  21776  mdetunilem8  21777  mdetunilem9  21778  cpmatacl  21874  cpmatmcllem  21876  mp2pm2mplem4  21967  en2top  22144  toponmre  22253  topssnei  22284  innei  22285  clslp  22308  restcls  22341  restntr  22342  ordtrest2lem  22363  cnpco  22427  cncls2  22433  cncnpi  22438  cncnp  22440  cnconst2  22443  cnpdis  22453  lmcnp  22464  cnhaus  22514  isreg2  22537  cncmp  22552  tgcmp  22561  sscmp  22565  cmpfi  22568  cnconn  22582  iunconnlem  22587  clsconn  22590  1stcfb  22605  1stcrest  22613  2ndcctbss  22615  2ndcdisj  22616  1stcelcls  22621  1stccnp  22622  restnlly  22642  cldllycmp  22655  lly1stc  22656  dislly  22657  locfincmp  22686  comppfsc  22692  kgentopon  22698  kgenidm  22707  1stckgenlem  22713  kgencn3  22718  ptpjpre1  22731  ptbasin  22737  txcls  22764  tx2cn  22770  ptpjcn  22771  ptclsg  22775  ptcnp  22782  txdis  22792  txlly  22796  txnlly  22797  pthaus  22798  txtube  22800  txcmplem1  22801  txcmplem2  22802  txcmp  22803  txhaus  22807  txkgen  22812  xkohaus  22813  xkococnlem  22819  xkococn  22820  txconn  22849  qtopeu  22876  qtoprest  22877  regr1lem2  22900  kqreglem1  22901  cmphaushmeo  22960  xkocnv  22974  fgabs  23039  filuni  23045  trufil  23070  ufileu  23079  filufint  23080  fin1aufil  23092  elfm2  23108  rnelfmlem  23112  fmfnfmlem2  23115  fmfnfmlem4  23117  fmufil  23119  flimopn  23135  fbflim2  23137  hausflimi  23140  hausflim  23141  flimcf  23142  flimclslem  23144  flimsncls  23146  hauspwpwf1  23147  cnpflfi  23159  fclsnei  23179  fclscf  23185  flimfnfcls  23188  fclscmp  23190  ufilcmp  23192  fcfnei  23195  cnpfcf  23201  alexsublem  23204  alexsub  23205  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem3  23214  ptcmplem4  23215  ptcmplem5  23216  symgtgp  23266  tgpconncompeqg  23272  tgpconncomp  23273  ghmcnp  23275  tgpt0  23279  qustgplem  23281  haustsms2  23297  tsmsgsum  23299  tsmsres  23304  tsmsxp  23315  imasdsf1olem  23535  xbln0  23576  blssps  23586  blss  23587  neibl  23666  blcld  23670  metss  23673  metequiv2  23675  met1stc  23686  metrest  23689  prdsxmslem2  23694  metcnp3  23705  nrmmetd  23739  nlmvscnlem1  23859  nrginvrcnlem  23864  nmoleub  23904  icccmplem2  23995  icccmp  23997  reconnlem2  23999  xrge0tsms  24006  metdstri  24023  metdseq0  24026  metdscn  24028  cnmpopc  24100  lebnumlem3  24135  pcoval2  24188  pcopt  24194  nmoleub2lem  24286  nmhmcn  24292  ipcnlem1  24418  cfilfcls  24447  cmetcaulem  24461  iscmet3lem2  24465  iscmet3  24466  equivcau  24473  caubl  24481  bcthlem2  24498  bcthlem3  24499  bcthlem4  24500  bcthlem5  24501  ivthlem2  24625  ivthlem3  24626  ovoliunlem2  24676  ovolicc2lem2  24691  ovolicc2lem5  24694  ovolicc2  24695  ismbl2  24700  nulmbl  24708  nulmbl2  24709  unmbl  24710  shftmbl  24711  voliunlem3  24725  volsup  24729  ioombl1lem4  24734  ioombl1  24735  icombl  24737  ioombl  24738  uniioombl  24762  opnmbllem  24774  volivth  24780  vitali  24786  mbflimsup  24839  i1fadd  24868  itg1addlem4  24872  itg1addlem4OLD  24873  itg2le  24913  itg2seq  24916  itg2lea  24918  itg2splitlem  24922  itg2split  24923  itg2mono  24927  itg2gt0  24934  itg2cnlem2  24936  itgss  24985  itgfsum  25000  itgcn  25018  ellimc3  25052  limcco  25066  limciun  25067  dvnres  25104  dvnfre  25125  rolle  25163  c1liplem1  25169  dvivth  25183  dvne0  25184  lhop1lem  25186  lhop1  25187  lhop  25189  dvcnvrelem1  25190  dvfsumrlim  25204  dvfsum2  25207  ftc1a  25210  ftc1lem6  25214  itgsubst  25222  tdeglem4  25233  tdeglem4OLD  25234  mdegaddle  25248  mdegvscale  25249  mdegmullem  25252  deg1tmle  25291  ply1divex  25310  dvdsq1p  25334  fta1g  25341  fta1b  25343  plyco0  25362  coeeulem  25394  dgrlem  25399  plyco  25411  coemullem  25420  dgreq0  25435  dgrco  25445  plydivex  25466  quotcan  25478  aannenlem1  25497  aalioulem2  25502  aalioulem3  25503  taylthlem1  25541  ulmbdd  25566  itgulm  25576  radcnvlt1  25586  psercnlem1  25593  abelthlem2  25600  abelthlem8  25607  logcnlem5  25810  efopn  25822  cxpmul2z  25855  cxpcn3lem  25909  cxpeq  25919  xrlimcnp  26127  cxplim  26130  o1cxp  26133  cxploglim  26136  scvxcvx  26144  jensen  26147  ftalem1  26231  ftalem2  26232  fta  26238  basellem3  26241  isppw2  26273  ppinprm  26310  chtnprm  26312  dvdsmulf1o  26352  chtublem  26368  perfectlem2  26387  dchrfi  26412  dchrptlem1  26421  dchrptlem2  26422  dchrptlem3  26423  dchrsum2  26425  bposlem1  26441  bposlem3  26443  2sqlem5  26579  2sqlem6  26580  2sqlem8  26583  2sqlem10  26585  2sqb  26589  chebbnd1lem1  26626  chtppilimlem2  26631  dchrisum0flb  26667  dchrisum0fno1  26668  dchrisum0  26677  pntrsumbnd2  26724  pntpbnd1  26743  pntpbnd2  26744  pntlemp  26767  pnt3  26769  qabvle  26782  ostth2lem2  26791  ostth3  26795  ostth  26796  colinearalglem4  27286  axcontlem10  27350  upgrex  27471  smcnlem  29068  ubthlem1  29241  ubthlem3  29243  htthlem  29288  5oalem6  30030  leopmuli  30504  pjnormssi  30539  pjclem4  30570  pj3si  30578  hatomistici  30733  sumdmdlem  30789  wrdt2ind  31234  xrge0tsmsd  31326  isarchiofld  31525  ordtrest2NEWlem  31881  qqhf  31945  eulerpartlemb  32344  ballotlemfc0  32468  ballotlemfcc  32469  sgn3da  32517  subfacp1lem5  33155  erdszelem7  33168  erdszelem11  33172  pconnconn  33202  txpconn  33203  connpconn  33206  sconnpi1  33210  txsconn  33212  cvxsconn  33214  cvmopnlem  33249  cvmfolem  33250  cvmliftmolem2  33253  cvmliftlem7  33262  cvmliftlem10  33265  cvmlift2lem10  33283  cvmlift3lem4  33293  cvmlift3lem8  33297  satfun  33382  msubff1  33527  wzel  33827  wsuclem  33828  naddssim  33846  nolt02o  33907  nogt01o  33908  nosupprefixmo  33912  noinfprefixmo  33913  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  noetasuplem4  33948  noetainflem4  33952  etasslt  34016  madebdaylemlrcut  34088  btwnouttr2  34333  cgrxfr  34366  btwnxfr  34367  brcolinear  34370  lineext  34387  btwnconn1lem13  34410  midofsegid  34415  segcon2  34416  brsegle  34419  seglecgr12im  34421  segletr  34425  colinbtwnle  34429  broutsideof2  34433  btwnoutside  34436  broutsideof3  34437  outsideoftr  34440  outsideofeq  34441  outsideofeu  34442  outsidele  34443  lineunray  34458  lineelsb2  34459  linethru  34464  finminlem  34516  nn0prpwlem  34520  neibastop2lem  34558  neibastop2  34559  neibastop3  34560  topjoin  34563  tailfb  34575  relowlssretop  35543  fvineqsneq  35592  wl-sbcom2d-lem1  35723  finixpnum  35771  poimirlem6  35792  poimirlem7  35793  poimirlem13  35799  poimirlem26  35812  poimirlem29  35815  heicant  35821  opnmbllem0  35822  mblfinlem3  35825  ismblfin  35827  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  itg2addnclem3  35839  ftc1cnnc  35858  sdclem2  35909  fdc  35912  istotbnd3  35938  isbnd2  35950  isbnd3  35951  prdsbnd  35960  cntotbnd  35963  heibor1lem  35976  heibor1  35977  heiborlem10  35987  rrncmslem  35999  ghomco  36058  1idl  36193  unichnidl  36198  prtlem10  36886  prtlem18  36898  atlatmstc  37340  cvrexchlem  37440  paddasslem14  37854  pexmidlem5N  37995  cdleme29ex  38395  cdlemefr29exN  38423  cdleme32fva  38458  diarnN  39150  dihlsscpre  39255  isnacs3  40539  fnwe2lem2  40883  kelac1  40895  hbtlem5  40960  hbt  40962  dgraa0p  40981  fzunt  41069  fzuntd  41070  monoordxrv  43029  rlimdmafv  44680  rlimdmafv2  44761  fmtnoprmfac2  45030  perfectALTVlem2  45185  mogoldbb  45248  mgmhmeql  45368  lindslinindsimp2  45815