Theorem expr 458

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  animpimp2impd  845  3expia  1122  rexlimdvaa  3157  reximddv  3172  disjxiun  5146  wereu2  5674  frpomin  6342  ordtr3  6410  fcof1  7285  knatar  7354  riota5f  7394  ovmpodf  7564  extmptsuppeq  8173  suppss  8179  suppssOLD  8180  suppss2  8185  frrlem14  8284  fprresex  8295  wfrlem17OLD  8325  smoord  8365  tfrlem9a  8386  oaass  8561  oelimcl  8600  oaabs2  8648  cofon1  8671  naddssim  8684  swoso  8736  eceqoveq  8816  domdifsn  9054  domunsncan  9072  omxpenlem  9073  enfixsn  9081  mapdom2  9148  frfi  9288  fofinf1o  9327  finsschain  9359  elfiun  9425  marypha1lem  9428  eqsupd  9452  eqinfd  9480  ordiso2  9510  ordtypelem6  9518  ordtypelem7  9519  ordtypelem10  9522  oismo  9535  wemapsolem  9545  brwdom2  9568  wdomtr  9570  unwdomg  9579  xpwdomg  9580  unxpwdom2  9583  cantnfval2  9664  cantnfle  9666  cantnflem1  9684  cantnf  9688  r1ordg  9773  tcrank  9879  carddomi2  9965  harval2  9992  infxpenlem  10008  infxpenc2lem2  10015  fseqenlem1  10019  dfac8clem  10027  acndom2  10049  infpwfien  10057  iunfictbso  10109  dfac12lem3  10140  infxp  10210  coflim  10256  cofsmo  10264  coftr  10268  sornom  10272  infpssrlem4  10301  enfin2i  10316  fin23lem26  10320  fin23lem27  10323  fin23lem36  10343  fin23lem40  10346  isf32lem5  10352  isf34lem4  10372  isfin1-3  10381  fin1a2lem10  10404  fin1a2lem13  10407  fin1a2s  10409  hsmexlem4  10424  ttukeylem5  10508  ttukeylem6  10509  ttukeylem7  10510  alephval2  10567  gchor  10622  fpwwe2lem6  10631  fpwwe2lem11  10636  fpwwe2  10638  pwfseqlem4a  10656  pwfseqlem4  10657  winalim2  10691  gchina  10694  inar1  10770  nqereq  10930  prlem934  11028  prlem936  11042  addsrmo  11068  mulsrmo  11069  supsrlem  11106  axpre-sup  11164  dedekind  11377  dedekindle  11378  mulge0b  12084  supaddc  12181  supmul1  12183  un0addcl  12505  un0mulcl  12506  uzwo3  12927  qbtwnre  13178  xlemul1a  13267  seqcl2  13986  seqfveq2  13990  seqshft2  13994  monoord  13998  seqsplit  14001  seqf1olem1  14007  seqid2  14014  seqhomo  14015  expnegz  14062  expcan  14134  ltexp2  14135  discr  14203  bcval5  14278  hashbc  14412  hashf1lem2  14417  seqcoll  14425  seqcoll2  14426  wrdind  14672  wrd2ind  14673  cau3lem  15301  ello1d  15467  lo1bdd2  15468  rlimclim  15490  climrlim2  15491  rlimdm  15495  rlimcn1  15532  reccn2  15541  rlimsqzlem  15595  lo1le  15598  caucvgrlem  15619  caurcvg2  15624  summolem2  15662  zsum  15664  fsum  15666  fsumf1o  15669  sumss  15670  fsumss  15671  fsumcl2lem  15677  fsumadd  15686  fsumcom2  15720  fsum0diag2  15729  fsummulc2  15730  fsumconst  15736  fsumrelem  15753  fsumrlim  15757  fsumo1  15758  divrcnv  15798  geomulcvg  15822  mertenslem2  15831  prodmolem2  15879  zprod  15881  fprod  15885  fprodf1o  15890  prodss  15891  fprodss  15892  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodconst  15922  fprodn0  15923  fprodcom2  15928  ruclem8  16180  dvds0lem  16210  dvdsnegb  16217  dvdssub2  16244  bitsf1  16387  bitsshft  16416  bezoutlem3  16483  bezoutlem4  16484  isprm5  16644  isprm6  16651  hashgcdeq  16722  modprminv  16732  modprminveq  16733  reumodprminv  16737  pcqmul  16786  pcqcl  16789  pcxnn0cl  16793  pcxcl  16794  pc2dvds  16812  pcadd  16822  pcmpt  16825  pockthg  16839  infpnlem1  16843  prmreclem5  16853  vdwlem2  16915  vdwlem9  16922  vdwlem10  16923  vdwlem12  16925  ramub  16946  0ram  16953  ramub1lem2  16960  ramub1  16961  ramcl  16962  mreexexd  17592  acsfn2  17607  iscatd  17617  catpropd  17653  setcmon  18037  pleval2i  18289  psss  18533  mgmidsssn0  18591  mhmeql  18707  frmdss2  18744  frmdup3  18748  grprcan  18858  dfgrp3lem  18921  mulgnn0ass  18990  isnsg3  19040  ghmpreima  19114  ghmeql  19115  gaorber  19172  f1omvdco2  19316  psgnunilem1  19361  psgnunilem2  19363  oddvds  19415  gexdvds  19452  sylow1lem1  19466  odcau  19472  pgpssslw  19482  sylow2alem2  19486  sylow2blem3  19490  fislw  19493  lsmmod  19543  efgredlem  19615  frgpup3  19646  gsumval3  19775  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsumzoppg  19812  gsum2d2lem  19841  ablfac1eulem  19942  pgpfac1lem5  19949  ablfaclem3  19957  issubdrg  20401  lss1d  20574  lmhmeql  20666  lspextmo  20667  lspsnat  20758  lsppratlem6  20765  islbs3  20768  lbsextlem4  20774  lidl1el  20841  cnsubrg  21005  gsumfsum  21012  prmirredlem  21042  znidomb  21117  frgpcyg  21129  cssmre  21246  dsmmsubg  21298  dsmmlss  21299  frlmsslsp  21351  lindff1  21375  lindfrn  21376  rnasclassa  21449  mvrf1  21545  mplsubglem  21558  mpllsslem  21559  mplcoe1  21592  mplcoe5  21595  gsummoncoe1  21828  mat1dimcrng  21979  mdetdiaglem  22100  mdetunilem7  22120  mdetunilem8  22121  mdetunilem9  22122  cpmatacl  22218  cpmatmcllem  22220  mp2pm2mplem4  22311  en2top  22488  toponmre  22597  topssnei  22628  innei  22629  clslp  22652  restcls  22685  restntr  22686  ordtrest2lem  22707  cnpco  22771  cncls2  22777  cncnpi  22782  cncnp  22784  cnconst2  22787  cnpdis  22797  lmcnp  22808  cnhaus  22858  isreg2  22881  cncmp  22896  tgcmp  22905  sscmp  22909  cmpfi  22912  cnconn  22926  iunconnlem  22931  clsconn  22934  1stcfb  22949  1stcrest  22957  2ndcctbss  22959  2ndcdisj  22960  1stcelcls  22965  1stccnp  22966  restnlly  22986  cldllycmp  22999  lly1stc  23000  dislly  23001  locfincmp  23030  comppfsc  23036  kgentopon  23042  kgenidm  23051  1stckgenlem  23057  kgencn3  23062  ptpjpre1  23075  ptbasin  23081  txcls  23108  tx2cn  23114  ptpjcn  23115  ptclsg  23119  ptcnp  23126  txdis  23136  txlly  23140  txnlly  23141  pthaus  23142  txtube  23144  txcmplem1  23145  txcmplem2  23146  txcmp  23147  txhaus  23151  txkgen  23156  xkohaus  23157  xkococnlem  23163  xkococn  23164  txconn  23193  qtopeu  23220  qtoprest  23221  regr1lem2  23244  kqreglem1  23245  cmphaushmeo  23304  xkocnv  23318  fgabs  23383  filuni  23389  trufil  23414  ufileu  23423  filufint  23424  fin1aufil  23436  elfm2  23452  rnelfmlem  23456  fmfnfmlem2  23459  fmfnfmlem4  23461  fmufil  23463  flimopn  23479  fbflim2  23481  hausflimi  23484  hausflim  23485  flimcf  23486  flimclslem  23488  flimsncls  23490  hauspwpwf1  23491  cnpflfi  23503  fclsnei  23523  fclscf  23529  flimfnfcls  23532  fclscmp  23534  ufilcmp  23536  fcfnei  23539  cnpfcf  23545  alexsublem  23548  alexsub  23549  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem4  23559  ptcmplem5  23560  symgtgp  23610  tgpconncompeqg  23616  tgpconncomp  23617  ghmcnp  23619  tgpt0  23623  qustgplem  23625  haustsms2  23641  tsmsgsum  23643  tsmsres  23648  tsmsxp  23659  imasdsf1olem  23879  xbln0  23920  blssps  23930  blss  23931  neibl  24010  blcld  24014  metss  24017  metequiv2  24019  met1stc  24030  metrest  24033  prdsxmslem2  24038  metcnp3  24049  nrmmetd  24083  nlmvscnlem1  24203  nrginvrcnlem  24208  nmoleub  24248  icccmplem2  24339  icccmp  24341  reconnlem2  24343  xrge0tsms  24350  metdstri  24367  metdseq0  24370  metdscn  24372  cnmpopc  24444  lebnumlem3  24479  pcoval2  24532  pcopt  24538  nmoleub2lem  24630  nmhmcn  24636  ipcnlem1  24762  cfilfcls  24791  cmetcaulem  24805  iscmet3lem2  24809  iscmet3  24810  equivcau  24817  caubl  24825  bcthlem2  24842  bcthlem3  24843  bcthlem4  24844  bcthlem5  24845  ivthlem2  24969  ivthlem3  24970  ovoliunlem2  25020  ovolicc2lem2  25035  ovolicc2lem5  25038  ovolicc2  25039  ismbl2  25044  nulmbl  25052  nulmbl2  25053  unmbl  25054  shftmbl  25055  voliunlem3  25069  volsup  25073  ioombl1lem4  25078  ioombl1  25079  icombl  25081  ioombl  25082  uniioombl  25106  opnmbllem  25118  volivth  25124  vitali  25130  mbflimsup  25183  i1fadd  25212  itg1addlem4  25216  itg1addlem4OLD  25217  itg2le  25257  itg2seq  25260  itg2lea  25262  itg2splitlem  25266  itg2split  25267  itg2mono  25271  itg2gt0  25278  itg2cnlem2  25280  itgss  25329  itgfsum  25344  itgcn  25362  ellimc3  25396  limcco  25410  limciun  25411  dvnres  25448  dvnfre  25469  rolle  25507  c1liplem1  25513  dvivth  25527  dvne0  25528  lhop1lem  25530  lhop1  25531  lhop  25533  dvcnvrelem1  25534  dvfsumrlim  25548  dvfsum2  25551  ftc1a  25554  ftc1lem6  25558  itgsubst  25566  tdeglem4  25577  tdeglem4OLD  25578  mdegaddle  25592  mdegvscale  25593  mdegmullem  25596  deg1tmle  25635  ply1divex  25654  dvdsq1p  25678  fta1g  25685  fta1b  25687  plyco0  25706  coeeulem  25738  dgrlem  25743  plyco  25755  coemullem  25764  dgreq0  25779  dgrco  25789  plydivex  25810  quotcan  25822  aannenlem1  25841  aalioulem2  25846  aalioulem3  25847  taylthlem1  25885  ulmbdd  25910  itgulm  25920  radcnvlt1  25930  psercnlem1  25937  abelthlem2  25944  abelthlem8  25951  logcnlem5  26154  efopn  26166  cxpmul2z  26199  cxpcn3lem  26255  cxpeq  26265  xrlimcnp  26473  cxplim  26476  o1cxp  26479  cxploglim  26482  scvxcvx  26490  jensen  26493  ftalem1  26577  ftalem2  26578  fta  26584  basellem3  26587  isppw2  26619  ppinprm  26656  chtnprm  26658  dvdsmulf1o  26698  chtublem  26714  perfectlem2  26733  dchrfi  26758  dchrptlem1  26767  dchrptlem2  26768  dchrptlem3  26769  dchrsum2  26771  bposlem1  26787  bposlem3  26789  2sqlem5  26925  2sqlem6  26926  2sqlem8  26929  2sqlem10  26931  2sqb  26935  chebbnd1lem1  26972  chtppilimlem2  26977  dchrisum0flb  27013  dchrisum0fno1  27014  dchrisum0  27023  pntrsumbnd2  27070  pntpbnd1  27089  pntpbnd2  27090  pntlemp  27113  pnt3  27115  qabvle  27128  ostth2lem2  27137  ostth3  27141  ostth  27142  nolt02o  27198  nogt01o  27199  nosupprefixmo  27203  noinfprefixmo  27204  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  etasslt  27314  cuteq1  27334  madebdaylemlrcut  27393  cutlt  27419  mulsuniflem  27604  colinearalglem4  28167  axcontlem10  28231  upgrex  28352  smcnlem  29950  ubthlem1  30123  ubthlem3  30125  htthlem  30170  5oalem6  30912  leopmuli  31386  pjnormssi  31421  pjclem4  31452  pj3si  31460  hatomistici  31615  sumdmdlem  31671  wrdt2ind  32117  xrge0tsmsd  32209  isarchiofld  32435  ordtrest2NEWlem  32902  qqhf  32966  eulerpartlemb  33367  ballotlemfc0  33491  ballotlemfcc  33492  sgn3da  33540  subfacp1lem5  34175  erdszelem7  34188  erdszelem11  34192  pconnconn  34222  txpconn  34223  connpconn  34226  sconnpi1  34230  txsconn  34232  cvxsconn  34234  cvmopnlem  34269  cvmfolem  34270  cvmliftmolem2  34273  cvmliftlem7  34282  cvmliftlem10  34285  cvmlift2lem10  34303  cvmlift3lem4  34313  cvmlift3lem8  34317  satfun  34402  msubff1  34547  wzel  34796  wsuclem  34797  btwnouttr2  34994  cgrxfr  35027  btwnxfr  35028  brcolinear  35031  lineext  35048  btwnconn1lem13  35071  midofsegid  35076  segcon2  35077  brsegle  35080  seglecgr12im  35082  segletr  35086  colinbtwnle  35090  broutsideof2  35094  btwnoutside  35097  broutsideof3  35098  outsideoftr  35101  outsideofeq  35102  outsideofeu  35103  outsidele  35104  lineunray  35119  lineelsb2  35120  linethru  35125  finminlem  35203  nn0prpwlem  35207  neibastop2lem  35245  neibastop2  35246  neibastop3  35247  topjoin  35250  tailfb  35262  relowlssretop  36244  fvineqsneq  36293  wl-sbcom2d-lem1  36424  finixpnum  36473  poimirlem6  36494  poimirlem7  36495  poimirlem13  36501  poimirlem26  36514  poimirlem29  36517  heicant  36523  opnmbllem0  36524  mblfinlem3  36527  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnclem  36539  itg2addnclem3  36541  ftc1cnnc  36560  sdclem2  36610  fdc  36613  istotbnd3  36639  isbnd2  36651  isbnd3  36652  prdsbnd  36661  cntotbnd  36664  heibor1lem  36677  heibor1  36678  heiborlem10  36688  rrncmslem  36700  ghomco  36759  1idl  36894  unichnidl  36899  disjlem18  37670  prtlem10  37735  prtlem18  37747  atlatmstc  38189  cvrexchlem  38290  paddasslem14  38704  pexmidlem5N  38845  cdleme29ex  39245  cdlemefr29exN  39273  cdleme32fva  39308  diarnN  40000  dihlsscpre  40105  isnacs3  41448  fnwe2lem2  41793  kelac1  41805  hbtlem5  41870  hbt  41872  dgraa0p  41891  ofoafg  42104  ofoafo  42106  naddcnffo  42114  fzunt  42206  fzuntd  42207  monoordxrv  44192  rlimdmafv  45885  rlimdmafv2  45966  fmtnoprmfac2  46235  perfectALTVlem2  46390  mogoldbb  46453  mgmhmeql  46573  lindslinindsimp2  47144