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  3135  reximddv  3149  disjxiun  5099  wereu2  5628  frpomin  6301  ordtr3  6366  fcof1  7244  knatar  7314  riota5f  7354  ovmpodf  7525  extmptsuppeq  8144  suppss  8150  suppss2  8156  frrlem14  8255  fprresex  8266  smoord  8311  tfrlem9a  8331  oaass  8502  oelimcl  8541  oaabs2  8590  cofon1  8613  naddssim  8626  swoso  8682  eceqoveq  8772  domdifsn  9001  domunsncan  9018  omxpenlem  9019  enfixsn  9027  mapdom2  9089  frfi  9208  fofinf1o  9259  finsschain  9286  elfiun  9357  marypha1lem  9360  eqsupd  9384  eqinfd  9413  ordiso2  9444  ordtypelem6  9452  ordtypelem7  9453  ordtypelem10  9456  oismo  9469  wemapsolem  9479  brwdom2  9502  wdomtr  9504  unwdomg  9513  xpwdomg  9514  unxpwdom2  9517  cantnfval2  9598  cantnfle  9600  cantnflem1  9618  cantnf  9622  r1ordg  9707  tcrank  9813  carddomi2  9899  harval2  9926  infxpenlem  9942  infxpenc2lem2  9949  fseqenlem1  9953  dfac8clem  9961  acndom2  9983  infpwfien  9991  iunfictbso  10043  dfac12lem3  10075  infxp  10143  coflim  10190  cofsmo  10198  coftr  10202  sornom  10206  infpssrlem4  10235  enfin2i  10250  fin23lem26  10254  fin23lem27  10257  fin23lem36  10277  fin23lem40  10280  isf32lem5  10286  isf34lem4  10306  isfin1-3  10315  fin1a2lem10  10338  fin1a2lem13  10341  fin1a2s  10343  hsmexlem4  10358  ttukeylem5  10442  ttukeylem6  10443  ttukeylem7  10444  alephval2  10501  gchor  10556  fpwwe2lem6  10565  fpwwe2lem11  10570  fpwwe2  10572  pwfseqlem4a  10590  pwfseqlem4  10591  winalim2  10625  gchina  10628  inar1  10704  nqereq  10864  prlem934  10962  prlem936  10976  addsrmo  11002  mulsrmo  11003  supsrlem  11040  axpre-sup  11098  dedekind  11313  dedekindle  11314  mulge0b  12029  supaddc  12126  supmul1  12128  un0addcl  12451  un0mulcl  12452  uzwo3  12878  qbtwnre  13135  xlemul1a  13224  seqcl2  13961  seqfveq2  13965  seqshft2  13969  monoord  13973  seqsplit  13976  seqf1olem1  13982  seqid2  13989  seqhomo  13990  expnegz  14037  expcan  14110  ltexp2  14111  discr  14181  bcval5  14259  hashbc  14394  hashf1lem2  14397  seqcoll  14405  seqcoll2  14406  wrdind  14663  wrd2ind  14664  cau3lem  15297  ello1d  15465  lo1bdd2  15466  rlimclim  15488  climrlim2  15489  rlimdm  15493  rlimcn1  15530  reccn2  15539  rlimsqzlem  15591  lo1le  15594  caucvgrlem  15615  caurcvg2  15620  summolem2  15658  zsum  15660  fsum  15662  fsumf1o  15665  sumss  15666  fsumss  15667  fsumcl2lem  15673  fsumadd  15682  fsumcom2  15716  fsum0diag2  15725  fsummulc2  15726  fsumconst  15732  fsumrelem  15749  fsumrlim  15753  fsumo1  15754  divrcnv  15794  geomulcvg  15818  mertenslem2  15827  prodmolem2  15877  zprod  15879  fprod  15883  fprodf1o  15888  prodss  15889  fprodss  15890  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodconst  15920  fprodn0  15921  fprodcom2  15926  ruclem8  16181  dvds0lem  16212  dvdsnegb  16219  dvdssub2  16247  bitsf1  16392  bitsshft  16421  bezoutlem3  16487  bezoutlem4  16488  isprm5  16653  isprm6  16660  hashgcdeq  16736  modprminv  16746  modprminveq  16747  reumodprminv  16751  pcqmul  16800  pcqcl  16803  pcxnn0cl  16807  pcxcl  16808  pc2dvds  16826  pcadd  16836  pcmpt  16839  pockthg  16853  infpnlem1  16857  prmreclem5  16867  vdwlem2  16929  vdwlem9  16936  vdwlem10  16937  vdwlem12  16939  ramub  16960  0ram  16967  ramub1lem2  16974  ramub1  16975  ramcl  16976  mreexexd  17589  acsfn2  17604  iscatd  17614  catpropd  17650  setcmon  18029  pleval2i  18275  psss  18521  mgmidsssn0  18581  mgmhmeql  18625  mhmeql  18735  frmdss2  18772  frmdup3  18776  grprcan  18887  dfgrp3lem  18952  mulgnn0ass  19024  isnsg3  19074  ghmpreima  19152  ghmeql  19153  gaorber  19222  f1omvdco2  19362  psgnunilem1  19407  psgnunilem2  19409  oddvds  19461  gexdvds  19498  sylow1lem1  19512  odcau  19518  pgpssslw  19528  sylow2alem2  19532  sylow2blem3  19536  fislw  19539  lsmmod  19589  efgredlem  19661  frgpup3  19692  gsumval3  19821  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  gsum2d2lem  19887  ablfac1eulem  19988  pgpfac1lem5  19995  ablfaclem3  20003  issubdrg  20700  lss1d  20901  lmhmeql  20994  lspextmo  20995  lspsnat  21087  lsppratlem6  21094  islbs3  21097  lbsextlem4  21103  lidl1el  21168  cnsubrg  21369  gsumfsum  21376  prmirredlem  21414  znidomb  21503  frgpcyg  21515  cssmre  21635  dsmmsubg  21685  dsmmlss  21686  frlmsslsp  21738  lindff1  21762  lindfrn  21763  rnasclassa  21837  mvrf1  21928  mplsubglem  21941  mpllsslem  21942  mplcoe1  21977  mplcoe5  21980  gsummoncoe1  22228  mat1dimcrng  22397  mdetdiaglem  22518  mdetunilem7  22538  mdetunilem8  22539  mdetunilem9  22540  cpmatacl  22636  cpmatmcllem  22638  mp2pm2mplem4  22729  en2top  22905  toponmre  23013  topssnei  23044  innei  23045  clslp  23068  restcls  23101  restntr  23102  ordtrest2lem  23123  cnpco  23187  cncls2  23193  cncnpi  23198  cncnp  23200  cnconst2  23203  cnpdis  23213  lmcnp  23224  cnhaus  23274  isreg2  23297  cncmp  23312  tgcmp  23321  sscmp  23325  cmpfi  23328  cnconn  23342  iunconnlem  23347  clsconn  23350  1stcfb  23365  1stcrest  23373  2ndcctbss  23375  2ndcdisj  23376  1stcelcls  23381  1stccnp  23382  restnlly  23402  cldllycmp  23415  lly1stc  23416  dislly  23417  locfincmp  23446  comppfsc  23452  kgentopon  23458  kgenidm  23467  1stckgenlem  23473  kgencn3  23478  ptpjpre1  23491  ptbasin  23497  txcls  23524  tx2cn  23530  ptpjcn  23531  ptclsg  23535  ptcnp  23542  txdis  23552  txlly  23556  txnlly  23557  pthaus  23558  txtube  23560  txcmplem1  23561  txcmplem2  23562  txcmp  23563  txhaus  23567  txkgen  23572  xkohaus  23573  xkococnlem  23579  xkococn  23580  txconn  23609  qtopeu  23636  qtoprest  23637  regr1lem2  23660  kqreglem1  23661  cmphaushmeo  23720  xkocnv  23734  fgabs  23799  filuni  23805  trufil  23830  ufileu  23839  filufint  23840  fin1aufil  23852  elfm2  23868  rnelfmlem  23872  fmfnfmlem2  23875  fmfnfmlem4  23877  fmufil  23879  flimopn  23895  fbflim2  23897  hausflimi  23900  hausflim  23901  flimcf  23902  flimclslem  23904  flimsncls  23906  hauspwpwf1  23907  cnpflfi  23919  fclsnei  23939  fclscf  23945  flimfnfcls  23948  fclscmp  23950  ufilcmp  23952  fcfnei  23955  cnpfcf  23961  alexsublem  23964  alexsub  23965  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem3  23974  ptcmplem4  23975  ptcmplem5  23976  symgtgp  24026  tgpconncompeqg  24032  tgpconncomp  24033  ghmcnp  24035  tgpt0  24039  qustgplem  24041  haustsms2  24057  tsmsgsum  24059  tsmsres  24064  tsmsxp  24075  imasdsf1olem  24294  xbln0  24335  blssps  24345  blss  24346  neibl  24422  blcld  24426  metss  24429  metequiv2  24431  met1stc  24442  metrest  24445  prdsxmslem2  24450  metcnp3  24461  nrmmetd  24495  nlmvscnlem1  24607  nrginvrcnlem  24612  nmoleub  24652  icccmplem2  24745  icccmp  24747  reconnlem2  24749  xrge0tsms  24756  metdstri  24773  metdseq0  24776  metdscn  24778  cnmpopc  24855  lebnumlem3  24895  pcoval2  24949  pcopt  24955  nmoleub2lem  25047  nmhmcn  25053  ipcnlem1  25178  cfilfcls  25207  cmetcaulem  25221  iscmet3lem2  25225  iscmet3  25226  equivcau  25233  caubl  25241  bcthlem2  25258  bcthlem3  25259  bcthlem4  25260  bcthlem5  25261  ivthlem2  25386  ivthlem3  25387  ovoliunlem2  25437  ovolicc2lem2  25452  ovolicc2lem5  25455  ovolicc2  25456  ismbl2  25461  nulmbl  25469  nulmbl2  25470  unmbl  25471  shftmbl  25472  voliunlem3  25486  volsup  25490  ioombl1lem4  25495  ioombl1  25496  icombl  25498  ioombl  25499  uniioombl  25523  opnmbllem  25535  volivth  25541  vitali  25547  mbflimsup  25600  i1fadd  25629  itg1addlem4  25633  itg2le  25673  itg2seq  25676  itg2lea  25678  itg2splitlem  25682  itg2split  25683  itg2mono  25687  itg2gt0  25694  itg2cnlem2  25696  itgss  25746  itgfsum  25761  itgcn  25779  ellimc3  25813  limcco  25827  limciun  25828  dvnres  25866  dvnfre  25889  rolle  25927  c1liplem1  25934  dvivth  25948  dvne0  25949  lhop1lem  25951  lhop1  25952  lhop  25954  dvcnvrelem1  25955  dvfsumrlim  25971  dvfsum2  25974  ftc1a  25977  ftc1lem6  25981  itgsubst  25989  tdeglem4  25998  mdegaddle  26012  mdegvscale  26013  mdegmullem  26016  deg1tmle  26056  ply1divex  26075  dvdsq1p  26101  fta1g  26108  fta1b  26110  plyco0  26130  coeeulem  26162  dgrlem  26167  plyco  26179  coemullem  26188  dgreq0  26204  dgrco  26214  plydivex  26238  quotcan  26250  aannenlem1  26269  aalioulem2  26274  aalioulem3  26275  taylthlem1  26314  ulmbdd  26340  itgulm  26350  radcnvlt1  26360  psercnlem1  26368  abelthlem2  26375  abelthlem8  26382  logcnlem5  26588  efopn  26600  cxpmul2z  26633  cxpcn3lem  26690  cxpeq  26700  xrlimcnp  26911  cxplim  26915  o1cxp  26918  cxploglim  26921  scvxcvx  26929  jensen  26932  ftalem1  27016  ftalem2  27017  fta  27023  basellem3  27026  isppw2  27058  ppinprm  27095  chtnprm  27097  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chtublem  27155  perfectlem2  27174  dchrfi  27199  dchrptlem1  27208  dchrptlem2  27209  dchrptlem3  27210  dchrsum2  27212  bposlem1  27228  bposlem3  27230  2sqlem5  27366  2sqlem6  27367  2sqlem8  27370  2sqlem10  27372  2sqb  27376  chebbnd1lem1  27413  chtppilimlem2  27418  dchrisum0flb  27454  dchrisum0fno1  27455  dchrisum0  27464  pntrsumbnd2  27511  pntpbnd1  27530  pntpbnd2  27531  pntlemp  27554  pnt3  27556  qabvle  27569  ostth2lem2  27578  ostth3  27582  ostth  27583  nolt02o  27640  nogt01o  27641  nosupprefixmo  27645  noinfprefixmo  27646  nosupbnd1lem3  27655  nosupbnd1lem4  27656  nosupbnd1lem5  27657  noinfbnd1lem3  27670  noinfbnd1lem4  27671  noinfbnd1lem5  27672  noetasuplem4  27681  noetainflem4  27685  etasslt  27759  cuteq1  27783  madebdaylemlrcut  27848  cutlt  27880  mulsuniflem  28092  bdayon  28213  om2noseqlt  28233  n0sfincut  28286  zs12ge0  28395  readdscl  28403  remulscl  28406  colinearalglem4  28889  axcontlem10  28953  upgrex  29072  smcnlem  30676  ubthlem1  30849  ubthlem3  30851  htthlem  30896  5oalem6  31638  leopmuli  32112  pjnormssi  32147  pjclem4  32178  pj3si  32186  hatomistici  32341  sumdmdlem  32397  sgn3da  32809  wrdt2ind  32925  xrge0tsmsd  33045  isarchiofld  33168  ordtrest2NEWlem  33905  qqhf  33969  eulerpartlemb  34352  ballotlemfc0  34477  ballotlemfcc  34478  subfacp1lem5  35164  erdszelem7  35177  erdszelem11  35181  pconnconn  35211  txpconn  35212  connpconn  35215  sconnpi1  35219  txsconn  35221  cvxsconn  35223  cvmopnlem  35258  cvmfolem  35259  cvmliftmolem2  35262  cvmliftlem7  35271  cvmliftlem10  35274  cvmlift2lem10  35292  cvmlift3lem4  35302  cvmlift3lem8  35306  satfun  35391  msubff1  35536  wzel  35805  wsuclem  35806  btwnouttr2  36003  cgrxfr  36036  btwnxfr  36037  brcolinear  36040  lineext  36057  btwnconn1lem13  36080  midofsegid  36085  segcon2  36086  brsegle  36089  seglecgr12im  36091  segletr  36095  colinbtwnle  36099  broutsideof2  36103  btwnoutside  36106  broutsideof3  36107  outsideoftr  36110  outsideofeq  36111  outsideofeu  36112  outsidele  36113  lineunray  36128  lineelsb2  36129  linethru  36134  finminlem  36299  nn0prpwlem  36303  neibastop2lem  36341  neibastop2  36342  neibastop3  36343  topjoin  36346  tailfb  36358  relowlssretop  37344  fvineqsneq  37393  wl-sbcom2d-lem1  37540  finixpnum  37592  poimirlem6  37613  poimirlem7  37614  poimirlem13  37620  poimirlem26  37633  poimirlem29  37636  heicant  37642  opnmbllem0  37643  mblfinlem3  37646  ismblfin  37648  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  itg2addnclem3  37660  ftc1cnnc  37679  sdclem2  37729  fdc  37732  istotbnd3  37758  isbnd2  37770  isbnd3  37771  prdsbnd  37780  cntotbnd  37783  heibor1lem  37796  heibor1  37797  heiborlem10  37807  rrncmslem  37819  ghomco  37878  1idl  38013  unichnidl  38018  disjlem18  38785  prtlem10  38851  prtlem18  38863  atlatmstc  39305  cvrexchlem  39406  paddasslem14  39820  pexmidlem5N  39961  cdleme29ex  40361  cdlemefr29exN  40389  cdleme32fva  40424  diarnN  41116  dihlsscpre  41221  isnacs3  42691  fnwe2lem2  43033  kelac1  43045  hbtlem5  43110  hbt  43112  dgraa0p  43131  ofoafg  43336  ofoafo  43338  naddcnffo  43346  fzunt  43437  fzuntd  43438  monoordxrv  45470  rlimdmafv  47171  rlimdmafv2  47252  fmtnoprmfac2  47561  perfectALTVlem2  47716  mogoldbb  47779  lindslinindsimp2  48445