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 206  df-an 396

This theorem is referenced by:  animpimp2impd  845  3expia  1119  rexlimdvaa  3151  reximddv  3166  disjxiun  5139  wereu2  5669  frpomin  6340  ordtr3  6408  fcof1  7290  knatar  7359  riota5f  7399  ovmpodf  7571  extmptsuppeq  8186  suppss  8192  suppssOLD  8193  suppss2  8199  frrlem14  8298  fprresex  8309  wfrlem17OLD  8339  smoord  8379  tfrlem9a  8400  oaass  8575  oelimcl  8614  oaabs2  8663  cofon1  8686  naddssim  8699  swoso  8751  eceqoveq  8832  domdifsn  9070  domunsncan  9088  omxpenlem  9089  enfixsn  9097  mapdom2  9164  frfi  9304  fofinf1o  9343  finsschain  9375  elfiun  9445  marypha1lem  9448  eqsupd  9472  eqinfd  9500  ordiso2  9530  ordtypelem6  9538  ordtypelem7  9539  ordtypelem10  9542  oismo  9555  wemapsolem  9565  brwdom2  9588  wdomtr  9590  unwdomg  9599  xpwdomg  9600  unxpwdom2  9603  cantnfval2  9684  cantnfle  9686  cantnflem1  9704  cantnf  9708  r1ordg  9793  tcrank  9899  carddomi2  9985  harval2  10012  infxpenlem  10028  infxpenc2lem2  10035  fseqenlem1  10039  dfac8clem  10047  acndom2  10069  infpwfien  10077  iunfictbso  10129  dfac12lem3  10160  infxp  10230  coflim  10276  cofsmo  10284  coftr  10288  sornom  10292  infpssrlem4  10321  enfin2i  10336  fin23lem26  10340  fin23lem27  10343  fin23lem36  10363  fin23lem40  10366  isf32lem5  10372  isf34lem4  10392  isfin1-3  10401  fin1a2lem10  10424  fin1a2lem13  10427  fin1a2s  10429  hsmexlem4  10444  ttukeylem5  10528  ttukeylem6  10529  ttukeylem7  10530  alephval2  10587  gchor  10642  fpwwe2lem6  10651  fpwwe2lem11  10656  fpwwe2  10658  pwfseqlem4a  10676  pwfseqlem4  10677  winalim2  10711  gchina  10714  inar1  10790  nqereq  10950  prlem934  11048  prlem936  11062  addsrmo  11088  mulsrmo  11089  supsrlem  11126  axpre-sup  11184  dedekind  11399  dedekindle  11400  mulge0b  12106  supaddc  12203  supmul1  12205  un0addcl  12527  un0mulcl  12528  uzwo3  12949  qbtwnre  13202  xlemul1a  13291  seqcl2  14009  seqfveq2  14013  seqshft2  14017  monoord  14021  seqsplit  14024  seqf1olem1  14030  seqid2  14037  seqhomo  14038  expnegz  14085  expcan  14157  ltexp2  14158  discr  14226  bcval5  14301  hashbc  14436  hashf1lem2  14441  seqcoll  14449  seqcoll2  14450  wrdind  14696  wrd2ind  14697  cau3lem  15325  ello1d  15491  lo1bdd2  15492  rlimclim  15514  climrlim2  15515  rlimdm  15519  rlimcn1  15556  reccn2  15565  rlimsqzlem  15619  lo1le  15622  caucvgrlem  15643  caurcvg2  15648  summolem2  15686  zsum  15688  fsum  15690  fsumf1o  15693  sumss  15694  fsumss  15695  fsumcl2lem  15701  fsumadd  15710  fsumcom2  15744  fsum0diag2  15753  fsummulc2  15754  fsumconst  15760  fsumrelem  15777  fsumrlim  15781  fsumo1  15782  divrcnv  15822  geomulcvg  15846  mertenslem2  15855  prodmolem2  15903  zprod  15905  fprod  15909  fprodf1o  15914  prodss  15915  fprodss  15916  fprodcl2lem  15918  fprodmul  15928  fproddiv  15929  fprodconst  15946  fprodn0  15947  fprodcom2  15952  ruclem8  16205  dvds0lem  16235  dvdsnegb  16242  dvdssub2  16269  bitsf1  16412  bitsshft  16441  bezoutlem3  16508  bezoutlem4  16509  isprm5  16669  isprm6  16676  hashgcdeq  16749  modprminv  16759  modprminveq  16760  reumodprminv  16764  pcqmul  16813  pcqcl  16816  pcxnn0cl  16820  pcxcl  16821  pc2dvds  16839  pcadd  16849  pcmpt  16852  pockthg  16866  infpnlem1  16870  prmreclem5  16880  vdwlem2  16942  vdwlem9  16949  vdwlem10  16950  vdwlem12  16952  ramub  16973  0ram  16980  ramub1lem2  16987  ramub1  16988  ramcl  16989  mreexexd  17619  acsfn2  17634  iscatd  17644  catpropd  17680  setcmon  18067  pleval2i  18319  psss  18563  mgmidsssn0  18623  mgmhmeql  18667  mhmeql  18769  frmdss2  18806  frmdup3  18810  grprcan  18921  dfgrp3lem  18985  mulgnn0ass  19056  isnsg3  19106  ghmpreima  19183  ghmeql  19184  gaorber  19250  f1omvdco2  19394  psgnunilem1  19439  psgnunilem2  19441  oddvds  19493  gexdvds  19530  sylow1lem1  19544  odcau  19550  pgpssslw  19560  sylow2alem2  19564  sylow2blem3  19568  fislw  19571  lsmmod  19621  efgredlem  19693  frgpup3  19724  gsumval3  19853  gsumzres  19855  gsumzcl2  19856  gsumzf1o  19858  gsumzaddlem  19867  gsumconst  19880  gsumzmhm  19883  gsumzoppg  19890  gsum2d2lem  19919  ablfac1eulem  20020  pgpfac1lem5  20027  ablfaclem3  20035  issubdrg  20657  lss1d  20836  lmhmeql  20929  lspextmo  20930  lspsnat  21022  lsppratlem6  21029  islbs3  21032  lbsextlem4  21038  lidl1el  21111  cnsubrg  21347  gsumfsum  21354  prmirredlem  21385  znidomb  21482  frgpcyg  21494  cssmre  21612  dsmmsubg  21664  dsmmlss  21665  frlmsslsp  21717  lindff1  21741  lindfrn  21742  rnasclassa  21815  mvrf1  21915  mplsubglem  21928  mpllsslem  21929  mplcoe1  21962  mplcoe5  21965  gsummoncoe1  22214  mat1dimcrng  22366  mdetdiaglem  22487  mdetunilem7  22507  mdetunilem8  22508  mdetunilem9  22509  cpmatacl  22605  cpmatmcllem  22607  mp2pm2mplem4  22698  en2top  22875  toponmre  22984  topssnei  23015  innei  23016  clslp  23039  restcls  23072  restntr  23073  ordtrest2lem  23094  cnpco  23158  cncls2  23164  cncnpi  23169  cncnp  23171  cnconst2  23174  cnpdis  23184  lmcnp  23195  cnhaus  23245  isreg2  23268  cncmp  23283  tgcmp  23292  sscmp  23296  cmpfi  23299  cnconn  23313  iunconnlem  23318  clsconn  23321  1stcfb  23336  1stcrest  23344  2ndcctbss  23346  2ndcdisj  23347  1stcelcls  23352  1stccnp  23353  restnlly  23373  cldllycmp  23386  lly1stc  23387  dislly  23388  locfincmp  23417  comppfsc  23423  kgentopon  23429  kgenidm  23438  1stckgenlem  23444  kgencn3  23449  ptpjpre1  23462  ptbasin  23468  txcls  23495  tx2cn  23501  ptpjcn  23502  ptclsg  23506  ptcnp  23513  txdis  23523  txlly  23527  txnlly  23528  pthaus  23529  txtube  23531  txcmplem1  23532  txcmplem2  23533  txcmp  23534  txhaus  23538  txkgen  23543  xkohaus  23544  xkococnlem  23550  xkococn  23551  txconn  23580  qtopeu  23607  qtoprest  23608  regr1lem2  23631  kqreglem1  23632  cmphaushmeo  23691  xkocnv  23705  fgabs  23770  filuni  23776  trufil  23801  ufileu  23810  filufint  23811  fin1aufil  23823  elfm2  23839  rnelfmlem  23843  fmfnfmlem2  23846  fmfnfmlem4  23848  fmufil  23850  flimopn  23866  fbflim2  23868  hausflimi  23871  hausflim  23872  flimcf  23873  flimclslem  23875  flimsncls  23877  hauspwpwf1  23878  cnpflfi  23890  fclsnei  23910  fclscf  23916  flimfnfcls  23919  fclscmp  23921  ufilcmp  23923  fcfnei  23926  cnpfcf  23932  alexsublem  23935  alexsub  23936  alexsubALTlem2  23939  alexsubALTlem3  23940  alexsubALTlem4  23941  ptcmplem3  23945  ptcmplem4  23946  ptcmplem5  23947  symgtgp  23997  tgpconncompeqg  24003  tgpconncomp  24004  ghmcnp  24006  tgpt0  24010  qustgplem  24012  haustsms2  24028  tsmsgsum  24030  tsmsres  24035  tsmsxp  24046  imasdsf1olem  24266  xbln0  24307  blssps  24317  blss  24318  neibl  24397  blcld  24401  metss  24404  metequiv2  24406  met1stc  24417  metrest  24420  prdsxmslem2  24425  metcnp3  24436  nrmmetd  24470  nlmvscnlem1  24590  nrginvrcnlem  24595  nmoleub  24635  icccmplem2  24726  icccmp  24728  reconnlem2  24730  xrge0tsms  24737  metdstri  24754  metdseq0  24757  metdscn  24759  cnmpopc  24836  lebnumlem3  24876  pcoval2  24930  pcopt  24936  nmoleub2lem  25028  nmhmcn  25034  ipcnlem1  25160  cfilfcls  25189  cmetcaulem  25203  iscmet3lem2  25207  iscmet3  25208  equivcau  25215  caubl  25223  bcthlem2  25240  bcthlem3  25241  bcthlem4  25242  bcthlem5  25243  ivthlem2  25368  ivthlem3  25369  ovoliunlem2  25419  ovolicc2lem2  25434  ovolicc2lem5  25437  ovolicc2  25438  ismbl2  25443  nulmbl  25451  nulmbl2  25452  unmbl  25453  shftmbl  25454  voliunlem3  25468  volsup  25472  ioombl1lem4  25477  ioombl1  25478  icombl  25480  ioombl  25481  uniioombl  25505  opnmbllem  25517  volivth  25523  vitali  25529  mbflimsup  25582  i1fadd  25611  itg1addlem4  25615  itg1addlem4OLD  25616  itg2le  25656  itg2seq  25659  itg2lea  25661  itg2splitlem  25665  itg2split  25666  itg2mono  25670  itg2gt0  25677  itg2cnlem2  25679  itgss  25728  itgfsum  25743  itgcn  25761  ellimc3  25795  limcco  25809  limciun  25810  dvnres  25848  dvnfre  25871  rolle  25909  c1liplem1  25916  dvivth  25930  dvne0  25931  lhop1lem  25933  lhop1  25934  lhop  25936  dvcnvrelem1  25937  dvfsumrlim  25953  dvfsum2  25956  ftc1a  25959  ftc1lem6  25963  itgsubst  25971  tdeglem4  25982  tdeglem4OLD  25983  mdegaddle  25997  mdegvscale  25998  mdegmullem  26001  deg1tmle  26040  ply1divex  26059  dvdsq1p  26084  fta1g  26091  fta1b  26093  plyco0  26113  coeeulem  26145  dgrlem  26150  plyco  26162  coemullem  26171  dgreq0  26187  dgrco  26197  plydivex  26219  quotcan  26231  aannenlem1  26250  aalioulem2  26255  aalioulem3  26256  taylthlem1  26295  ulmbdd  26321  itgulm  26331  radcnvlt1  26341  psercnlem1  26349  abelthlem2  26356  abelthlem8  26363  logcnlem5  26567  efopn  26579  cxpmul2z  26612  cxpcn3lem  26669  cxpeq  26679  xrlimcnp  26887  cxplim  26891  o1cxp  26894  cxploglim  26897  scvxcvx  26905  jensen  26908  ftalem1  26992  ftalem2  26993  fta  26999  basellem3  27002  isppw2  27034  ppinprm  27071  chtnprm  27073  mpodvdsmulf1o  27113  dvdsmulf1o  27115  chtublem  27131  perfectlem2  27150  dchrfi  27175  dchrptlem1  27184  dchrptlem2  27185  dchrptlem3  27186  dchrsum2  27188  bposlem1  27204  bposlem3  27206  2sqlem5  27342  2sqlem6  27343  2sqlem8  27346  2sqlem10  27348  2sqb  27352  chebbnd1lem1  27389  chtppilimlem2  27394  dchrisum0flb  27430  dchrisum0fno1  27431  dchrisum0  27440  pntrsumbnd2  27487  pntpbnd1  27506  pntpbnd2  27507  pntlemp  27530  pnt3  27532  qabvle  27545  ostth2lem2  27554  ostth3  27558  ostth  27559  nolt02o  27615  nogt01o  27616  nosupprefixmo  27620  noinfprefixmo  27621  nosupbnd1lem3  27630  nosupbnd1lem4  27631  nosupbnd1lem5  27632  noinfbnd1lem3  27645  noinfbnd1lem4  27646  noinfbnd1lem5  27647  noetasuplem4  27656  noetainflem4  27660  etasslt  27733  cuteq1  27753  madebdaylemlrcut  27812  cutlt  27839  mulsuniflem  28036  om2noseqlt  28159  readdscl  28214  remulscl  28217  colinearalglem4  28707  axcontlem10  28771  upgrex  28892  smcnlem  30494  ubthlem1  30667  ubthlem3  30669  htthlem  30714  5oalem6  31456  leopmuli  31930  pjnormssi  31965  pjclem4  31996  pj3si  32004  hatomistici  32159  sumdmdlem  32215  wrdt2ind  32656  xrge0tsmsd  32749  isarchiofld  32972  ordtrest2NEWlem  33459  qqhf  33523  eulerpartlemb  33924  ballotlemfc0  34048  ballotlemfcc  34049  sgn3da  34097  subfacp1lem5  34730  erdszelem7  34743  erdszelem11  34747  pconnconn  34777  txpconn  34778  connpconn  34781  sconnpi1  34785  txsconn  34787  cvxsconn  34789  cvmopnlem  34824  cvmfolem  34825  cvmliftmolem2  34828  cvmliftlem7  34837  cvmliftlem10  34840  cvmlift2lem10  34858  cvmlift3lem4  34868  cvmlift3lem8  34872  satfun  34957  msubff1  35102  wzel  35356  wsuclem  35357  btwnouttr2  35554  cgrxfr  35587  btwnxfr  35588  brcolinear  35591  lineext  35608  btwnconn1lem13  35631  midofsegid  35636  segcon2  35637  brsegle  35640  seglecgr12im  35642  segletr  35646  colinbtwnle  35650  broutsideof2  35654  btwnoutside  35657  broutsideof3  35658  outsideoftr  35661  outsideofeq  35662  outsideofeu  35663  outsidele  35664  lineunray  35679  lineelsb2  35680  linethru  35685  finminlem  35738  nn0prpwlem  35742  neibastop2lem  35780  neibastop2  35781  neibastop3  35782  topjoin  35785  tailfb  35797  relowlssretop  36778  fvineqsneq  36827  wl-sbcom2d-lem1  36961  finixpnum  37013  poimirlem6  37034  poimirlem7  37035  poimirlem13  37041  poimirlem26  37054  poimirlem29  37057  heicant  37063  opnmbllem0  37064  mblfinlem3  37067  ismblfin  37069  ovoliunnfl  37070  voliunnfl  37072  volsupnfl  37073  itg2addnclem  37079  itg2addnclem3  37081  ftc1cnnc  37100  sdclem2  37150  fdc  37153  istotbnd3  37179  isbnd2  37191  isbnd3  37192  prdsbnd  37201  cntotbnd  37204  heibor1lem  37217  heibor1  37218  heiborlem10  37228  rrncmslem  37240  ghomco  37299  1idl  37434  unichnidl  37439  disjlem18  38209  prtlem10  38274  prtlem18  38286  atlatmstc  38728  cvrexchlem  38829  paddasslem14  39243  pexmidlem5N  39384  cdleme29ex  39784  cdlemefr29exN  39812  cdleme32fva  39847  diarnN  40539  dihlsscpre  40644  isnacs3  42052  fnwe2lem2  42397  kelac1  42409  hbtlem5  42474  hbt  42476  dgraa0p  42495  ofoafg  42706  ofoafo  42708  naddcnffo  42716  fzunt  42808  fzuntd  42809  monoordxrv  44787  rlimdmafv  46480  rlimdmafv2  46561  fmtnoprmfac2  46830  perfectALTVlem2  46985  mogoldbb  47048  lindslinindsimp2  47454