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  3143  reximddv  3158  disjxiun  5122  wereu2  5664  frpomin  6342  ordtr3  6410  fcof1  7290  knatar  7360  riota5f  7399  ovmpodf  7572  extmptsuppeq  8196  suppss  8202  suppss2  8208  frrlem14  8307  fprresex  8318  wfrlem17OLD  8348  smoord  8388  tfrlem9a  8409  oaass  8582  oelimcl  8621  oaabs2  8670  cofon1  8693  naddssim  8706  swoso  8762  eceqoveq  8845  domdifsn  9077  domunsncan  9095  omxpenlem  9096  enfixsn  9104  mapdom2  9171  frfi  9304  fofinf1o  9355  finsschain  9382  elfiun  9453  marypha1lem  9456  eqsupd  9480  eqinfd  9508  ordiso2  9538  ordtypelem6  9546  ordtypelem7  9547  ordtypelem10  9550  oismo  9563  wemapsolem  9573  brwdom2  9596  wdomtr  9598  unwdomg  9607  xpwdomg  9608  unxpwdom2  9611  cantnfval2  9692  cantnfle  9694  cantnflem1  9712  cantnf  9716  r1ordg  9801  tcrank  9907  carddomi2  9993  harval2  10020  infxpenlem  10036  infxpenc2lem2  10043  fseqenlem1  10047  dfac8clem  10055  acndom2  10077  infpwfien  10085  iunfictbso  10137  dfac12lem3  10169  infxp  10237  coflim  10284  cofsmo  10292  coftr  10296  sornom  10300  infpssrlem4  10329  enfin2i  10344  fin23lem26  10348  fin23lem27  10351  fin23lem36  10371  fin23lem40  10374  isf32lem5  10380  isf34lem4  10400  isfin1-3  10409  fin1a2lem10  10432  fin1a2lem13  10435  fin1a2s  10437  hsmexlem4  10452  ttukeylem5  10536  ttukeylem6  10537  ttukeylem7  10538  alephval2  10595  gchor  10650  fpwwe2lem6  10659  fpwwe2lem11  10664  fpwwe2  10666  pwfseqlem4a  10684  pwfseqlem4  10685  winalim2  10719  gchina  10722  inar1  10798  nqereq  10958  prlem934  11056  prlem936  11070  addsrmo  11096  mulsrmo  11097  supsrlem  11134  axpre-sup  11192  dedekind  11407  dedekindle  11408  mulge0b  12121  supaddc  12218  supmul1  12220  un0addcl  12543  un0mulcl  12544  uzwo3  12968  qbtwnre  13224  xlemul1a  13313  seqcl2  14044  seqfveq2  14048  seqshft2  14052  monoord  14056  seqsplit  14059  seqf1olem1  14065  seqid2  14072  seqhomo  14073  expnegz  14120  expcan  14192  ltexp2  14193  discr  14262  bcval5  14340  hashbc  14475  hashf1lem2  14478  seqcoll  14486  seqcoll2  14487  wrdind  14743  wrd2ind  14744  cau3lem  15376  ello1d  15542  lo1bdd2  15543  rlimclim  15565  climrlim2  15566  rlimdm  15570  rlimcn1  15607  reccn2  15616  rlimsqzlem  15668  lo1le  15671  caucvgrlem  15692  caurcvg2  15697  summolem2  15735  zsum  15737  fsum  15739  fsumf1o  15742  sumss  15743  fsumss  15744  fsumcl2lem  15750  fsumadd  15759  fsumcom2  15793  fsum0diag2  15802  fsummulc2  15803  fsumconst  15809  fsumrelem  15826  fsumrlim  15830  fsumo1  15831  divrcnv  15871  geomulcvg  15895  mertenslem2  15904  prodmolem2  15954  zprod  15956  fprod  15960  fprodf1o  15965  prodss  15966  fprodss  15967  fprodcl2lem  15969  fprodmul  15979  fproddiv  15980  fprodconst  15997  fprodn0  15998  fprodcom2  16003  ruclem8  16256  dvds0lem  16287  dvdsnegb  16294  dvdssub2  16321  bitsf1  16466  bitsshft  16495  bezoutlem3  16561  bezoutlem4  16562  isprm5  16727  isprm6  16734  hashgcdeq  16810  modprminv  16820  modprminveq  16821  reumodprminv  16825  pcqmul  16874  pcqcl  16877  pcxnn0cl  16881  pcxcl  16882  pc2dvds  16900  pcadd  16910  pcmpt  16913  pockthg  16927  infpnlem1  16931  prmreclem5  16941  vdwlem2  17003  vdwlem9  17010  vdwlem10  17011  vdwlem12  17013  ramub  17034  0ram  17041  ramub1lem2  17048  ramub1  17049  ramcl  17050  mreexexd  17667  acsfn2  17682  iscatd  17692  catpropd  17728  setcmon  18108  pleval2i  18355  psss  18599  mgmidsssn0  18659  mgmhmeql  18703  mhmeql  18813  frmdss2  18850  frmdup3  18854  grprcan  18965  dfgrp3lem  19030  mulgnn0ass  19102  isnsg3  19152  ghmpreima  19230  ghmeql  19231  gaorber  19300  f1omvdco2  19439  psgnunilem1  19484  psgnunilem2  19486  oddvds  19538  gexdvds  19575  sylow1lem1  19589  odcau  19595  pgpssslw  19605  sylow2alem2  19609  sylow2blem3  19613  fislw  19616  lsmmod  19666  efgredlem  19738  frgpup3  19769  gsumval3  19898  gsumzres  19900  gsumzcl2  19901  gsumzf1o  19903  gsumzaddlem  19912  gsumconst  19925  gsumzmhm  19928  gsumzoppg  19935  gsum2d2lem  19964  ablfac1eulem  20065  pgpfac1lem5  20072  ablfaclem3  20080  issubdrg  20754  lss1d  20934  lmhmeql  21027  lspextmo  21028  lspsnat  21120  lsppratlem6  21127  islbs3  21130  lbsextlem4  21136  lidl1el  21203  cnsubrg  21412  gsumfsum  21419  prmirredlem  21450  znidomb  21547  frgpcyg  21559  cssmre  21678  dsmmsubg  21730  dsmmlss  21731  frlmsslsp  21783  lindff1  21807  lindfrn  21808  rnasclassa  21882  mvrf1  21973  mplsubglem  21986  mpllsslem  21987  mplcoe1  22022  mplcoe5  22025  gsummoncoe1  22279  mat1dimcrng  22450  mdetdiaglem  22571  mdetunilem7  22591  mdetunilem8  22592  mdetunilem9  22593  cpmatacl  22689  cpmatmcllem  22691  mp2pm2mplem4  22782  en2top  22958  toponmre  23066  topssnei  23097  innei  23098  clslp  23121  restcls  23154  restntr  23155  ordtrest2lem  23176  cnpco  23240  cncls2  23246  cncnpi  23251  cncnp  23253  cnconst2  23256  cnpdis  23266  lmcnp  23277  cnhaus  23327  isreg2  23350  cncmp  23365  tgcmp  23374  sscmp  23378  cmpfi  23381  cnconn  23395  iunconnlem  23400  clsconn  23403  1stcfb  23418  1stcrest  23426  2ndcctbss  23428  2ndcdisj  23429  1stcelcls  23434  1stccnp  23435  restnlly  23455  cldllycmp  23468  lly1stc  23469  dislly  23470  locfincmp  23499  comppfsc  23505  kgentopon  23511  kgenidm  23520  1stckgenlem  23526  kgencn3  23531  ptpjpre1  23544  ptbasin  23550  txcls  23577  tx2cn  23583  ptpjcn  23584  ptclsg  23588  ptcnp  23595  txdis  23605  txlly  23609  txnlly  23610  pthaus  23611  txtube  23613  txcmplem1  23614  txcmplem2  23615  txcmp  23616  txhaus  23620  txkgen  23625  xkohaus  23626  xkococnlem  23632  xkococn  23633  txconn  23662  qtopeu  23689  qtoprest  23690  regr1lem2  23713  kqreglem1  23714  cmphaushmeo  23773  xkocnv  23787  fgabs  23852  filuni  23858  trufil  23883  ufileu  23892  filufint  23893  fin1aufil  23905  elfm2  23921  rnelfmlem  23925  fmfnfmlem2  23928  fmfnfmlem4  23930  fmufil  23932  flimopn  23948  fbflim2  23950  hausflimi  23953  hausflim  23954  flimcf  23955  flimclslem  23957  flimsncls  23959  hauspwpwf1  23960  cnpflfi  23972  fclsnei  23992  fclscf  23998  flimfnfcls  24001  fclscmp  24003  ufilcmp  24005  fcfnei  24008  cnpfcf  24014  alexsublem  24017  alexsub  24018  alexsubALTlem2  24021  alexsubALTlem3  24022  alexsubALTlem4  24023  ptcmplem3  24027  ptcmplem4  24028  ptcmplem5  24029  symgtgp  24079  tgpconncompeqg  24085  tgpconncomp  24086  ghmcnp  24088  tgpt0  24092  qustgplem  24094  haustsms2  24110  tsmsgsum  24112  tsmsres  24117  tsmsxp  24128  imasdsf1olem  24347  xbln0  24388  blssps  24398  blss  24399  neibl  24477  blcld  24481  metss  24484  metequiv2  24486  met1stc  24497  metrest  24500  prdsxmslem2  24505  metcnp3  24516  nrmmetd  24550  nlmvscnlem1  24662  nrginvrcnlem  24667  nmoleub  24707  icccmplem2  24800  icccmp  24802  reconnlem2  24804  xrge0tsms  24811  metdstri  24828  metdseq0  24831  metdscn  24833  cnmpopc  24910  lebnumlem3  24950  pcoval2  25004  pcopt  25010  nmoleub2lem  25102  nmhmcn  25108  ipcnlem1  25234  cfilfcls  25263  cmetcaulem  25277  iscmet3lem2  25281  iscmet3  25282  equivcau  25289  caubl  25297  bcthlem2  25314  bcthlem3  25315  bcthlem4  25316  bcthlem5  25317  ivthlem2  25442  ivthlem3  25443  ovoliunlem2  25493  ovolicc2lem2  25508  ovolicc2lem5  25511  ovolicc2  25512  ismbl2  25517  nulmbl  25525  nulmbl2  25526  unmbl  25527  shftmbl  25528  voliunlem3  25542  volsup  25546  ioombl1lem4  25551  ioombl1  25552  icombl  25554  ioombl  25555  uniioombl  25579  opnmbllem  25591  volivth  25597  vitali  25603  mbflimsup  25656  i1fadd  25685  itg1addlem4  25689  itg2le  25729  itg2seq  25732  itg2lea  25734  itg2splitlem  25738  itg2split  25739  itg2mono  25743  itg2gt0  25750  itg2cnlem2  25752  itgss  25802  itgfsum  25817  itgcn  25835  ellimc3  25869  limcco  25883  limciun  25884  dvnres  25922  dvnfre  25945  rolle  25983  c1liplem1  25990  dvivth  26004  dvne0  26005  lhop1lem  26007  lhop1  26008  lhop  26010  dvcnvrelem1  26011  dvfsumrlim  26027  dvfsum2  26030  ftc1a  26033  ftc1lem6  26037  itgsubst  26045  tdeglem4  26054  mdegaddle  26068  mdegvscale  26069  mdegmullem  26072  deg1tmle  26112  ply1divex  26131  dvdsq1p  26157  fta1g  26164  fta1b  26166  plyco0  26186  coeeulem  26218  dgrlem  26223  plyco  26235  coemullem  26244  dgreq0  26260  dgrco  26270  plydivex  26294  quotcan  26306  aannenlem1  26325  aalioulem2  26330  aalioulem3  26331  taylthlem1  26370  ulmbdd  26396  itgulm  26406  radcnvlt1  26416  psercnlem1  26424  abelthlem2  26431  abelthlem8  26438  logcnlem5  26643  efopn  26655  cxpmul2z  26688  cxpcn3lem  26745  cxpeq  26755  xrlimcnp  26966  cxplim  26970  o1cxp  26973  cxploglim  26976  scvxcvx  26984  jensen  26987  ftalem1  27071  ftalem2  27072  fta  27078  basellem3  27081  isppw2  27113  ppinprm  27150  chtnprm  27152  mpodvdsmulf1o  27192  dvdsmulf1o  27194  chtublem  27210  perfectlem2  27229  dchrfi  27254  dchrptlem1  27263  dchrptlem2  27264  dchrptlem3  27265  dchrsum2  27267  bposlem1  27283  bposlem3  27285  2sqlem5  27421  2sqlem6  27422  2sqlem8  27425  2sqlem10  27427  2sqb  27431  chebbnd1lem1  27468  chtppilimlem2  27473  dchrisum0flb  27509  dchrisum0fno1  27510  dchrisum0  27519  pntrsumbnd2  27566  pntpbnd1  27585  pntpbnd2  27586  pntlemp  27609  pnt3  27611  qabvle  27624  ostth2lem2  27633  ostth3  27637  ostth  27638  nolt02o  27695  nogt01o  27696  nosupprefixmo  27700  noinfprefixmo  27701  nosupbnd1lem3  27710  nosupbnd1lem4  27711  nosupbnd1lem5  27712  noinfbnd1lem3  27725  noinfbnd1lem4  27726  noinfbnd1lem5  27727  noetasuplem4  27736  noetainflem4  27740  etasslt  27813  cuteq1  27833  madebdaylemlrcut  27892  cutlt  27921  mulsuniflem  28130  om2noseqlt  28260  readdscl  28386  remulscl  28389  colinearalglem4  28873  axcontlem10  28937  upgrex  29056  smcnlem  30663  ubthlem1  30836  ubthlem3  30838  htthlem  30883  5oalem6  31625  leopmuli  32099  pjnormssi  32134  pjclem4  32165  pj3si  32173  hatomistici  32328  sumdmdlem  32384  wrdt2ind  32885  xrge0tsmsd  33011  isarchiofld  33293  ordtrest2NEWlem  33862  qqhf  33928  eulerpartlemb  34311  ballotlemfc0  34436  ballotlemfcc  34437  sgn3da  34485  subfacp1lem5  35130  erdszelem7  35143  erdszelem11  35147  pconnconn  35177  txpconn  35178  connpconn  35181  sconnpi1  35185  txsconn  35187  cvxsconn  35189  cvmopnlem  35224  cvmfolem  35225  cvmliftmolem2  35228  cvmliftlem7  35237  cvmliftlem10  35240  cvmlift2lem10  35258  cvmlift3lem4  35268  cvmlift3lem8  35272  satfun  35357  msubff1  35502  wzel  35766  wsuclem  35767  btwnouttr2  35964  cgrxfr  35997  btwnxfr  35998  brcolinear  36001  lineext  36018  btwnconn1lem13  36041  midofsegid  36046  segcon2  36047  brsegle  36050  seglecgr12im  36052  segletr  36056  colinbtwnle  36060  broutsideof2  36064  btwnoutside  36067  broutsideof3  36068  outsideoftr  36071  outsideofeq  36072  outsideofeu  36073  outsidele  36074  lineunray  36089  lineelsb2  36090  linethru  36095  finminlem  36260  nn0prpwlem  36264  neibastop2lem  36302  neibastop2  36303  neibastop3  36304  topjoin  36307  tailfb  36319  relowlssretop  37305  fvineqsneq  37354  wl-sbcom2d-lem1  37501  finixpnum  37553  poimirlem6  37574  poimirlem7  37575  poimirlem13  37581  poimirlem26  37594  poimirlem29  37597  heicant  37603  opnmbllem0  37604  mblfinlem3  37607  ismblfin  37609  ovoliunnfl  37610  voliunnfl  37612  volsupnfl  37613  itg2addnclem  37619  itg2addnclem3  37621  ftc1cnnc  37640  sdclem2  37690  fdc  37693  istotbnd3  37719  isbnd2  37731  isbnd3  37732  prdsbnd  37741  cntotbnd  37744  heibor1lem  37757  heibor1  37758  heiborlem10  37768  rrncmslem  37780  ghomco  37839  1idl  37974  unichnidl  37979  disjlem18  38742  prtlem10  38807  prtlem18  38819  atlatmstc  39261  cvrexchlem  39362  paddasslem14  39776  pexmidlem5N  39917  cdleme29ex  40317  cdlemefr29exN  40345  cdleme32fva  40380  diarnN  41072  dihlsscpre  41177  isnacs3  42666  fnwe2lem2  43008  kelac1  43020  hbtlem5  43085  hbt  43087  dgraa0p  43106  ofoafg  43312  ofoafo  43314  naddcnffo  43322  fzunt  43413  fzuntd  43414  monoordxrv  45437  rlimdmafv  47135  rlimdmafv2  47216  fmtnoprmfac2  47500  perfectALTVlem2  47655  mogoldbb  47718  lindslinindsimp2  48326