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  847  3expia  1122  rexlimdvaa  3140  reximddv  3154  disjxiun  5097  wereu2  5629  frpomin  6306  ordtr3  6371  fcof1  7243  knatar  7313  riota5f  7353  ovmpodf  7524  extmptsuppeq  8140  suppss  8146  suppss2  8152  frrlem14  8251  fprresex  8262  smoord  8307  tfrlem9a  8327  oaass  8498  oelimcl  8538  oaabs2  8587  cofon1  8610  naddssim  8623  swoso  8680  eceqoveq  8771  domdifsn  9000  domunsncan  9017  omxpenlem  9018  enfixsn  9026  mapdom2  9088  frfi  9197  fofinf1o  9244  finsschain  9271  elfiun  9345  marypha1lem  9348  eqsupd  9372  eqinfd  9401  ordiso2  9432  ordtypelem6  9440  ordtypelem7  9441  ordtypelem10  9444  oismo  9457  wemapsolem  9467  brwdom2  9490  wdomtr  9492  unwdomg  9501  xpwdomg  9502  unxpwdom2  9505  cantnfval2  9590  cantnfle  9592  cantnflem1  9610  cantnf  9614  r1ordg  9702  tcrank  9808  carddomi2  9894  harval2  9921  infxpenlem  9935  infxpenc2lem2  9942  fseqenlem1  9946  dfac8clem  9954  acndom2  9976  infpwfien  9984  iunfictbso  10036  dfac12lem3  10068  infxp  10136  coflim  10183  cofsmo  10191  coftr  10195  sornom  10199  infpssrlem4  10228  enfin2i  10243  fin23lem26  10247  fin23lem27  10250  fin23lem36  10270  fin23lem40  10273  isf32lem5  10279  isf34lem4  10299  isfin1-3  10308  fin1a2lem10  10331  fin1a2lem13  10334  fin1a2s  10336  hsmexlem4  10351  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  alephval2  10495  gchor  10550  fpwwe2lem6  10559  fpwwe2lem11  10564  fpwwe2  10566  pwfseqlem4a  10584  pwfseqlem4  10585  winalim2  10619  gchina  10622  inar1  10698  nqereq  10858  prlem934  10956  prlem936  10970  addsrmo  10996  mulsrmo  10997  supsrlem  11034  axpre-sup  11092  dedekind  11308  dedekindle  11309  mulge0b  12024  supaddc  12121  supmul1  12123  un0addcl  12446  un0mulcl  12447  uzwo3  12868  qbtwnre  13126  xlemul1a  13215  seqcl2  13955  seqfveq2  13959  seqshft2  13963  monoord  13967  seqsplit  13970  seqf1olem1  13976  seqid2  13983  seqhomo  13984  expnegz  14031  expcan  14104  ltexp2  14105  discr  14175  bcval5  14253  hashbc  14388  hashf1lem2  14391  seqcoll  14399  seqcoll2  14400  wrdind  14657  wrd2ind  14658  cau3lem  15290  ello1d  15458  lo1bdd2  15459  rlimclim  15481  climrlim2  15482  rlimdm  15486  rlimcn1  15523  reccn2  15532  rlimsqzlem  15584  lo1le  15587  caucvgrlem  15608  caurcvg2  15613  summolem2  15651  zsum  15653  fsum  15655  fsumf1o  15658  sumss  15659  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  fsumcom2  15709  fsum0diag2  15718  fsummulc2  15719  fsumconst  15725  fsumrelem  15742  fsumrlim  15746  fsumo1  15747  divrcnv  15787  geomulcvg  15811  mertenslem2  15820  prodmolem2  15870  zprod  15872  fprod  15876  fprodf1o  15881  prodss  15882  fprodss  15883  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodconst  15913  fprodn0  15914  fprodcom2  15919  ruclem8  16174  dvds0lem  16205  dvdsnegb  16212  dvdssub2  16240  bitsf1  16385  bitsshft  16414  bezoutlem3  16480  bezoutlem4  16481  isprm5  16646  isprm6  16653  hashgcdeq  16729  modprminv  16739  modprminveq  16740  reumodprminv  16744  pcqmul  16793  pcqcl  16796  pcxnn0cl  16800  pcxcl  16801  pc2dvds  16819  pcadd  16829  pcmpt  16832  pockthg  16846  infpnlem1  16850  prmreclem5  16860  vdwlem2  16922  vdwlem9  16929  vdwlem10  16930  vdwlem12  16932  ramub  16953  0ram  16960  ramub1lem2  16967  ramub1  16968  ramcl  16969  mreexexd  17583  acsfn2  17598  iscatd  17608  catpropd  17644  setcmon  18023  pleval2i  18269  psss  18515  mgmidsssn0  18609  mgmhmeql  18653  mhmeql  18763  frmdss2  18800  frmdup3  18804  grprcan  18918  dfgrp3lem  18983  mulgnn0ass  19055  isnsg3  19104  ghmpreima  19182  ghmeql  19183  gaorber  19252  f1omvdco2  19392  psgnunilem1  19437  psgnunilem2  19439  oddvds  19491  gexdvds  19528  sylow1lem1  19542  odcau  19548  pgpssslw  19558  sylow2alem2  19562  sylow2blem3  19566  fislw  19569  lsmmod  19619  efgredlem  19691  frgpup3  19722  gsumval3  19851  gsumzres  19853  gsumzcl2  19854  gsumzf1o  19856  gsumzaddlem  19865  gsumconst  19878  gsumzmhm  19881  gsumzoppg  19888  gsum2d2lem  19917  ablfac1eulem  20018  pgpfac1lem5  20025  ablfaclem3  20033  issubdrg  20728  lss1d  20929  lmhmeql  21022  lspextmo  21023  lspsnat  21115  lsppratlem6  21122  islbs3  21125  lbsextlem4  21131  lidl1el  21196  cnsubrg  21397  gsumfsum  21404  prmirredlem  21442  znidomb  21531  frgpcyg  21543  cssmre  21663  dsmmsubg  21713  dsmmlss  21714  frlmsslsp  21766  lindff1  21790  lindfrn  21791  rnasclassa  21866  mvrf1  21956  mplsubglem  21969  mpllsslem  21970  mplcoe1  22007  mplcoe5  22010  gsummoncoe1  22267  mat1dimcrng  22436  mdetdiaglem  22557  mdetunilem7  22577  mdetunilem8  22578  mdetunilem9  22579  cpmatacl  22675  cpmatmcllem  22677  mp2pm2mplem4  22768  en2top  22944  toponmre  23052  topssnei  23083  innei  23084  clslp  23107  restcls  23140  restntr  23141  ordtrest2lem  23162  cnpco  23226  cncls2  23232  cncnpi  23237  cncnp  23239  cnconst2  23242  cnpdis  23252  lmcnp  23263  cnhaus  23313  isreg2  23336  cncmp  23351  tgcmp  23360  sscmp  23364  cmpfi  23367  cnconn  23381  iunconnlem  23386  clsconn  23389  1stcfb  23404  1stcrest  23412  2ndcctbss  23414  2ndcdisj  23415  1stcelcls  23420  1stccnp  23421  restnlly  23441  cldllycmp  23454  lly1stc  23455  dislly  23456  locfincmp  23485  comppfsc  23491  kgentopon  23497  kgenidm  23506  1stckgenlem  23512  kgencn3  23517  ptpjpre1  23530  ptbasin  23536  txcls  23563  tx2cn  23569  ptpjcn  23570  ptclsg  23574  ptcnp  23581  txdis  23591  txlly  23595  txnlly  23596  pthaus  23597  txtube  23599  txcmplem1  23600  txcmplem2  23601  txcmp  23602  txhaus  23606  txkgen  23611  xkohaus  23612  xkococnlem  23618  xkococn  23619  txconn  23648  qtopeu  23675  qtoprest  23676  regr1lem2  23699  kqreglem1  23700  cmphaushmeo  23759  xkocnv  23773  fgabs  23838  filuni  23844  trufil  23869  ufileu  23878  filufint  23879  fin1aufil  23891  elfm2  23907  rnelfmlem  23911  fmfnfmlem2  23914  fmfnfmlem4  23916  fmufil  23918  flimopn  23934  fbflim2  23936  hausflimi  23939  hausflim  23940  flimcf  23941  flimclslem  23943  flimsncls  23945  hauspwpwf1  23946  cnpflfi  23958  fclsnei  23978  fclscf  23984  flimfnfcls  23987  fclscmp  23989  ufilcmp  23991  fcfnei  23994  cnpfcf  24000  alexsublem  24003  alexsub  24004  alexsubALTlem2  24007  alexsubALTlem3  24008  alexsubALTlem4  24009  ptcmplem3  24013  ptcmplem4  24014  ptcmplem5  24015  symgtgp  24065  tgpconncompeqg  24071  tgpconncomp  24072  ghmcnp  24074  tgpt0  24078  qustgplem  24080  haustsms2  24096  tsmsgsum  24098  tsmsres  24103  tsmsxp  24114  imasdsf1olem  24332  xbln0  24373  blssps  24383  blss  24384  neibl  24460  blcld  24464  metss  24467  metequiv2  24469  met1stc  24480  metrest  24483  prdsxmslem2  24488  metcnp3  24499  nrmmetd  24533  nlmvscnlem1  24645  nrginvrcnlem  24650  nmoleub  24690  icccmplem2  24783  icccmp  24785  reconnlem2  24787  xrge0tsms  24794  metdstri  24811  metdseq0  24814  metdscn  24816  cnmpopc  24893  lebnumlem3  24933  pcoval2  24987  pcopt  24993  nmoleub2lem  25085  nmhmcn  25091  ipcnlem1  25216  cfilfcls  25245  cmetcaulem  25259  iscmet3lem2  25263  iscmet3  25264  equivcau  25271  caubl  25279  bcthlem2  25296  bcthlem3  25297  bcthlem4  25298  bcthlem5  25299  ivthlem2  25424  ivthlem3  25425  ovoliunlem2  25475  ovolicc2lem2  25490  ovolicc2lem5  25493  ovolicc2  25494  ismbl2  25499  nulmbl  25507  nulmbl2  25508  unmbl  25509  shftmbl  25510  voliunlem3  25524  volsup  25528  ioombl1lem4  25533  ioombl1  25534  icombl  25536  ioombl  25537  uniioombl  25561  opnmbllem  25573  volivth  25579  vitali  25585  mbflimsup  25638  i1fadd  25667  itg1addlem4  25671  itg2le  25711  itg2seq  25714  itg2lea  25716  itg2splitlem  25720  itg2split  25721  itg2mono  25725  itg2gt0  25732  itg2cnlem2  25734  itgss  25784  itgfsum  25799  itgcn  25817  ellimc3  25851  limcco  25865  limciun  25866  dvnres  25904  dvnfre  25927  rolle  25965  c1liplem1  25972  dvivth  25986  dvne0  25987  lhop1lem  25989  lhop1  25990  lhop  25992  dvcnvrelem1  25993  dvfsumrlim  26009  dvfsum2  26012  ftc1a  26015  ftc1lem6  26019  itgsubst  26027  tdeglem4  26036  mdegaddle  26050  mdegvscale  26051  mdegmullem  26054  deg1tmle  26094  ply1divex  26113  dvdsq1p  26139  fta1g  26146  fta1b  26148  plyco0  26168  coeeulem  26200  dgrlem  26205  plyco  26217  coemullem  26226  dgreq0  26242  dgrco  26252  plydivex  26276  quotcan  26288  aannenlem1  26307  aalioulem2  26312  aalioulem3  26313  taylthlem1  26352  ulmbdd  26378  itgulm  26388  radcnvlt1  26398  psercnlem1  26406  abelthlem2  26413  abelthlem8  26420  logcnlem5  26626  efopn  26638  cxpmul2z  26671  cxpcn3lem  26728  cxpeq  26738  xrlimcnp  26949  cxplim  26953  o1cxp  26956  cxploglim  26959  scvxcvx  26967  jensen  26970  ftalem1  27054  ftalem2  27055  fta  27061  basellem3  27064  isppw2  27096  ppinprm  27133  chtnprm  27135  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chtublem  27193  perfectlem2  27212  dchrfi  27237  dchrptlem1  27246  dchrptlem2  27247  dchrptlem3  27248  dchrsum2  27250  bposlem1  27266  bposlem3  27268  2sqlem5  27404  2sqlem6  27405  2sqlem8  27408  2sqlem10  27410  2sqb  27414  chebbnd1lem1  27451  chtppilimlem2  27456  dchrisum0flb  27492  dchrisum0fno1  27493  dchrisum0  27502  pntrsumbnd2  27549  pntpbnd1  27568  pntpbnd2  27569  pntlemp  27592  pnt3  27594  qabvle  27607  ostth2lem2  27616  ostth3  27620  ostth  27621  nolt02o  27678  nogt01o  27679  nosupprefixmo  27683  noinfprefixmo  27684  nosupbnd1lem3  27693  nosupbnd1lem4  27694  nosupbnd1lem5  27695  noinfbnd1lem3  27708  noinfbnd1lem4  27709  noinfbnd1lem5  27710  noetasuplem4  27719  noetainflem4  27723  etaslts  27804  cuteq1  27828  madebdaylemlrcut  27910  cutlt  27943  mulsuniflem  28160  bdayons  28287  addonbday  28290  om2noseqlt  28310  n0fincut  28366  bdaypw2n0bndlem  28474  bdayfinbndlem1  28478  z12sge0  28494  readdscl  28510  remulscl  28513  colinearalglem4  28998  axcontlem10  29062  upgrex  29181  smcnlem  30789  ubthlem1  30962  ubthlem3  30964  htthlem  31009  5oalem6  31751  leopmuli  32225  pjnormssi  32260  pjclem4  32291  pj3si  32299  hatomistici  32454  sumdmdlem  32510  sgn3da  32930  wrdt2ind  33050  xrge0tsmsd  33171  isarchiofld  33297  ordtrest2NEWlem  34104  qqhf  34168  eulerpartlemb  34550  ballotlemfc0  34675  ballotlemfcc  34676  subfacp1lem5  35404  erdszelem7  35417  erdszelem11  35421  pconnconn  35451  txpconn  35452  connpconn  35455  sconnpi1  35459  txsconn  35461  cvxsconn  35463  cvmopnlem  35498  cvmfolem  35499  cvmliftmolem2  35502  cvmliftlem7  35511  cvmliftlem10  35514  cvmlift2lem10  35532  cvmlift3lem4  35542  cvmlift3lem8  35546  satfun  35631  msubff1  35776  wzel  36042  wsuclem  36043  btwnouttr2  36242  cgrxfr  36275  btwnxfr  36276  brcolinear  36279  lineext  36296  btwnconn1lem13  36319  midofsegid  36324  segcon2  36325  brsegle  36328  seglecgr12im  36330  segletr  36334  colinbtwnle  36338  broutsideof2  36342  btwnoutside  36345  broutsideof3  36346  outsideoftr  36349  outsideofeq  36350  outsideofeu  36351  outsidele  36352  lineunray  36367  lineelsb2  36368  linethru  36373  finminlem  36538  nn0prpwlem  36542  neibastop2lem  36580  neibastop2  36581  neibastop3  36582  topjoin  36585  tailfb  36597  relowlssretop  37622  fvineqsneq  37671  wl-sbcom2d-lem1  37818  finixpnum  37860  poimirlem6  37881  poimirlem7  37882  poimirlem13  37888  poimirlem26  37901  poimirlem29  37904  heicant  37910  opnmbllem0  37911  mblfinlem3  37914  ismblfin  37916  ovoliunnfl  37917  voliunnfl  37919  volsupnfl  37920  itg2addnclem  37926  itg2addnclem3  37928  ftc1cnnc  37947  sdclem2  37997  fdc  38000  istotbnd3  38026  isbnd2  38038  isbnd3  38039  prdsbnd  38048  cntotbnd  38051  heibor1lem  38064  heibor1  38065  heiborlem10  38075  rrncmslem  38087  ghomco  38146  1idl  38281  unichnidl  38286  disjlem18  39158  prtlem10  39245  prtlem18  39257  atlatmstc  39699  cvrexchlem  39799  paddasslem14  40213  pexmidlem5N  40354  cdleme29ex  40754  cdlemefr29exN  40782  cdleme32fva  40817  diarnN  41509  dihlsscpre  41614  isnacs3  43071  fnwe2lem2  43412  kelac1  43424  hbtlem5  43489  hbt  43491  dgraa0p  43510  ofoafg  43715  ofoafo  43717  naddcnffo  43725  fzunt  43815  fzuntd  43816  monoordxrv  45843  rlimdmafv  47541  rlimdmafv2  47622  fmtnoprmfac2  47931  perfectALTVlem2  48086  mogoldbb  48149  lindslinindsimp2  48827