Theorem expr 455

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  animpimp2impd  844  3expia  1118  rexlimdvaa  3146  reximddv  3161  disjxiun  5145  wereu2  5674  frpomin  6346  ordtr3  6414  fcof1  7294  knatar  7362  riota5f  7402  ovmpodf  7575  extmptsuppeq  8191  suppss  8197  suppssOLD  8198  suppss2  8204  frrlem14  8303  fprresex  8314  wfrlem17OLD  8344  smoord  8384  tfrlem9a  8405  oaass  8580  oelimcl  8619  oaabs2  8668  cofon1  8691  naddssim  8704  swoso  8756  eceqoveq  8839  domdifsn  9077  domunsncan  9095  omxpenlem  9096  enfixsn  9104  mapdom2  9171  frfi  9311  fofinf1o  9351  finsschain  9383  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  10168  infxp  10238  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  12114  supaddc  12211  supmul1  12213  un0addcl  12535  un0mulcl  12536  uzwo3  12957  qbtwnre  13210  xlemul1a  13299  seqcl2  14017  seqfveq2  14021  seqshft2  14025  monoord  14029  seqsplit  14032  seqf1olem1  14038  seqid2  14045  seqhomo  14046  expnegz  14093  expcan  14165  ltexp2  14166  discr  14234  bcval5  14309  hashbc  14444  hashf1lem2  14449  seqcoll  14457  seqcoll2  14458  wrdind  14704  wrd2ind  14705  cau3lem  15333  ello1d  15499  lo1bdd2  15500  rlimclim  15522  climrlim2  15523  rlimdm  15527  rlimcn1  15564  reccn2  15573  rlimsqzlem  15627  lo1le  15630  caucvgrlem  15651  caurcvg2  15656  summolem2  15694  zsum  15696  fsum  15698  fsumf1o  15701  sumss  15702  fsumss  15703  fsumcl2lem  15709  fsumadd  15718  fsumcom2  15752  fsum0diag2  15761  fsummulc2  15762  fsumconst  15768  fsumrelem  15785  fsumrlim  15789  fsumo1  15790  divrcnv  15830  geomulcvg  15854  mertenslem2  15863  prodmolem2  15911  zprod  15913  fprod  15917  fprodf1o  15922  prodss  15923  fprodss  15924  fprodcl2lem  15926  fprodmul  15936  fproddiv  15937  fprodconst  15954  fprodn0  15955  fprodcom2  15960  ruclem8  16213  dvds0lem  16243  dvdsnegb  16250  dvdssub2  16277  bitsf1  16420  bitsshft  16449  bezoutlem3  16516  bezoutlem4  16517  isprm5  16677  isprm6  16684  hashgcdeq  16757  modprminv  16767  modprminveq  16768  reumodprminv  16772  pcqmul  16821  pcqcl  16824  pcxnn0cl  16828  pcxcl  16829  pc2dvds  16847  pcadd  16857  pcmpt  16860  pockthg  16874  infpnlem1  16878  prmreclem5  16888  vdwlem2  16950  vdwlem9  16957  vdwlem10  16958  vdwlem12  16960  ramub  16981  0ram  16988  ramub1lem2  16995  ramub1  16996  ramcl  16997  mreexexd  17627  acsfn2  17642  iscatd  17652  catpropd  17688  setcmon  18075  pleval2i  18327  psss  18571  mgmidsssn0  18631  mgmhmeql  18675  mhmeql  18782  frmdss2  18819  frmdup3  18823  grprcan  18934  dfgrp3lem  18998  mulgnn0ass  19069  isnsg3  19119  ghmpreima  19196  ghmeql  19197  gaorber  19263  f1omvdco2  19407  psgnunilem1  19452  psgnunilem2  19454  oddvds  19506  gexdvds  19543  sylow1lem1  19557  odcau  19563  pgpssslw  19573  sylow2alem2  19577  sylow2blem3  19581  fislw  19584  lsmmod  19634  efgredlem  19706  frgpup3  19737  gsumval3  19866  gsumzres  19868  gsumzcl2  19869  gsumzf1o  19871  gsumzaddlem  19880  gsumconst  19893  gsumzmhm  19896  gsumzoppg  19903  gsum2d2lem  19932  ablfac1eulem  20033  pgpfac1lem5  20040  ablfaclem3  20048  issubdrg  20672  lss1d  20851  lmhmeql  20944  lspextmo  20945  lspsnat  21037  lsppratlem6  21044  islbs3  21047  lbsextlem4  21053  lidl1el  21126  cnsubrg  21364  gsumfsum  21371  prmirredlem  21402  znidomb  21499  frgpcyg  21511  cssmre  21629  dsmmsubg  21681  dsmmlss  21682  frlmsslsp  21734  lindff1  21758  lindfrn  21759  rnasclassa  21832  mvrf1  21935  mplsubglem  21948  mpllsslem  21949  mplcoe1  21982  mplcoe5  21985  gsummoncoe1  22236  mat1dimcrng  22409  mdetdiaglem  22530  mdetunilem7  22550  mdetunilem8  22551  mdetunilem9  22552  cpmatacl  22648  cpmatmcllem  22650  mp2pm2mplem4  22741  en2top  22918  toponmre  23027  topssnei  23058  innei  23059  clslp  23082  restcls  23115  restntr  23116  ordtrest2lem  23137  cnpco  23201  cncls2  23207  cncnpi  23212  cncnp  23214  cnconst2  23217  cnpdis  23227  lmcnp  23238  cnhaus  23288  isreg2  23311  cncmp  23326  tgcmp  23335  sscmp  23339  cmpfi  23342  cnconn  23356  iunconnlem  23361  clsconn  23364  1stcfb  23379  1stcrest  23387  2ndcctbss  23389  2ndcdisj  23390  1stcelcls  23395  1stccnp  23396  restnlly  23416  cldllycmp  23429  lly1stc  23430  dislly  23431  locfincmp  23460  comppfsc  23466  kgentopon  23472  kgenidm  23481  1stckgenlem  23487  kgencn3  23492  ptpjpre1  23505  ptbasin  23511  txcls  23538  tx2cn  23544  ptpjcn  23545  ptclsg  23549  ptcnp  23556  txdis  23566  txlly  23570  txnlly  23571  pthaus  23572  txtube  23574  txcmplem1  23575  txcmplem2  23576  txcmp  23577  txhaus  23581  txkgen  23586  xkohaus  23587  xkococnlem  23593  xkococn  23594  txconn  23623  qtopeu  23650  qtoprest  23651  regr1lem2  23674  kqreglem1  23675  cmphaushmeo  23734  xkocnv  23748  fgabs  23813  filuni  23819  trufil  23844  ufileu  23853  filufint  23854  fin1aufil  23866  elfm2  23882  rnelfmlem  23886  fmfnfmlem2  23889  fmfnfmlem4  23891  fmufil  23893  flimopn  23909  fbflim2  23911  hausflimi  23914  hausflim  23915  flimcf  23916  flimclslem  23918  flimsncls  23920  hauspwpwf1  23921  cnpflfi  23933  fclsnei  23953  fclscf  23959  flimfnfcls  23962  fclscmp  23964  ufilcmp  23966  fcfnei  23969  cnpfcf  23975  alexsublem  23978  alexsub  23979  alexsubALTlem2  23982  alexsubALTlem3  23983  alexsubALTlem4  23984  ptcmplem3  23988  ptcmplem4  23989  ptcmplem5  23990  symgtgp  24040  tgpconncompeqg  24046  tgpconncomp  24047  ghmcnp  24049  tgpt0  24053  qustgplem  24055  haustsms2  24071  tsmsgsum  24073  tsmsres  24078  tsmsxp  24089  imasdsf1olem  24309  xbln0  24350  blssps  24360  blss  24361  neibl  24440  blcld  24444  metss  24447  metequiv2  24449  met1stc  24460  metrest  24463  prdsxmslem2  24468  metcnp3  24479  nrmmetd  24513  nlmvscnlem1  24633  nrginvrcnlem  24638  nmoleub  24678  icccmplem2  24769  icccmp  24771  reconnlem2  24773  xrge0tsms  24780  metdstri  24797  metdseq0  24800  metdscn  24802  cnmpopc  24879  lebnumlem3  24919  pcoval2  24973  pcopt  24979  nmoleub2lem  25071  nmhmcn  25077  ipcnlem1  25203  cfilfcls  25232  cmetcaulem  25246  iscmet3lem2  25250  iscmet3  25251  equivcau  25258  caubl  25266  bcthlem2  25283  bcthlem3  25284  bcthlem4  25285  bcthlem5  25286  ivthlem2  25411  ivthlem3  25412  ovoliunlem2  25462  ovolicc2lem2  25477  ovolicc2lem5  25480  ovolicc2  25481  ismbl2  25486  nulmbl  25494  nulmbl2  25495  unmbl  25496  shftmbl  25497  voliunlem3  25511  volsup  25515  ioombl1lem4  25520  ioombl1  25521  icombl  25523  ioombl  25524  uniioombl  25548  opnmbllem  25560  volivth  25566  vitali  25572  mbflimsup  25625  i1fadd  25654  itg1addlem4  25658  itg1addlem4OLD  25659  itg2le  25699  itg2seq  25702  itg2lea  25704  itg2splitlem  25708  itg2split  25709  itg2mono  25713  itg2gt0  25720  itg2cnlem2  25722  itgss  25771  itgfsum  25786  itgcn  25804  ellimc3  25838  limcco  25852  limciun  25853  dvnres  25891  dvnfre  25914  rolle  25952  c1liplem1  25959  dvivth  25973  dvne0  25974  lhop1lem  25976  lhop1  25977  lhop  25979  dvcnvrelem1  25980  dvfsumrlim  25996  dvfsum2  25999  ftc1a  26002  ftc1lem6  26006  itgsubst  26014  tdeglem4  26025  tdeglem4OLD  26026  mdegaddle  26040  mdegvscale  26041  mdegmullem  26044  deg1tmle  26083  ply1divex  26102  dvdsq1p  26127  fta1g  26134  fta1b  26136  plyco0  26156  coeeulem  26188  dgrlem  26193  plyco  26205  coemullem  26214  dgreq0  26230  dgrco  26240  plydivex  26262  quotcan  26274  aannenlem1  26293  aalioulem2  26298  aalioulem3  26299  taylthlem1  26338  ulmbdd  26364  itgulm  26374  radcnvlt1  26384  psercnlem1  26392  abelthlem2  26399  abelthlem8  26406  logcnlem5  26610  efopn  26622  cxpmul2z  26655  cxpcn3lem  26712  cxpeq  26722  xrlimcnp  26930  cxplim  26934  o1cxp  26937  cxploglim  26940  scvxcvx  26948  jensen  26951  ftalem1  27035  ftalem2  27036  fta  27042  basellem3  27045  isppw2  27077  ppinprm  27114  chtnprm  27116  mpodvdsmulf1o  27156  dvdsmulf1o  27158  chtublem  27174  perfectlem2  27193  dchrfi  27218  dchrptlem1  27227  dchrptlem2  27228  dchrptlem3  27229  dchrsum2  27231  bposlem1  27247  bposlem3  27249  2sqlem5  27385  2sqlem6  27386  2sqlem8  27389  2sqlem10  27391  2sqb  27395  chebbnd1lem1  27432  chtppilimlem2  27437  dchrisum0flb  27473  dchrisum0fno1  27474  dchrisum0  27483  pntrsumbnd2  27530  pntpbnd1  27549  pntpbnd2  27550  pntlemp  27573  pnt3  27575  qabvle  27588  ostth2lem2  27597  ostth3  27601  ostth  27602  nolt02o  27658  nogt01o  27659  nosupprefixmo  27663  noinfprefixmo  27664  nosupbnd1lem3  27673  nosupbnd1lem4  27674  nosupbnd1lem5  27675  noinfbnd1lem3  27688  noinfbnd1lem4  27689  noinfbnd1lem5  27690  noetasuplem4  27699  noetainflem4  27703  etasslt  27776  cuteq1  27796  madebdaylemlrcut  27855  cutlt  27882  mulsuniflem  28083  om2noseqlt  28206  readdscl  28283  remulscl  28286  colinearalglem4  28776  axcontlem10  28840  upgrex  28961  smcnlem  30563  ubthlem1  30736  ubthlem3  30738  htthlem  30783  5oalem6  31525  leopmuli  31999  pjnormssi  32034  pjclem4  32065  pj3si  32073  hatomistici  32228  sumdmdlem  32284  wrdt2ind  32731  xrge0tsmsd  32828  isarchiofld  33092  ordtrest2NEWlem  33593  qqhf  33657  eulerpartlemb  34058  ballotlemfc0  34182  ballotlemfcc  34183  sgn3da  34231  subfacp1lem5  34864  erdszelem7  34877  erdszelem11  34881  pconnconn  34911  txpconn  34912  connpconn  34915  sconnpi1  34919  txsconn  34921  cvxsconn  34923  cvmopnlem  34958  cvmfolem  34959  cvmliftmolem2  34962  cvmliftlem7  34971  cvmliftlem10  34974  cvmlift2lem10  34992  cvmlift3lem4  35002  cvmlift3lem8  35006  satfun  35091  msubff1  35236  wzel  35490  wsuclem  35491  btwnouttr2  35688  cgrxfr  35721  btwnxfr  35722  brcolinear  35725  lineext  35742  btwnconn1lem13  35765  midofsegid  35770  segcon2  35771  brsegle  35774  seglecgr12im  35776  segletr  35780  colinbtwnle  35784  broutsideof2  35788  btwnoutside  35791  broutsideof3  35792  outsideoftr  35795  outsideofeq  35796  outsideofeu  35797  outsidele  35798  lineunray  35813  lineelsb2  35814  linethru  35819  finminlem  35872  nn0prpwlem  35876  neibastop2lem  35914  neibastop2  35915  neibastop3  35916  topjoin  35919  tailfb  35931  relowlssretop  36912  fvineqsneq  36961  wl-sbcom2d-lem1  37096  finixpnum  37148  poimirlem6  37169  poimirlem7  37170  poimirlem13  37176  poimirlem26  37189  poimirlem29  37192  heicant  37198  opnmbllem0  37199  mblfinlem3  37202  ismblfin  37204  ovoliunnfl  37205  voliunnfl  37207  volsupnfl  37208  itg2addnclem  37214  itg2addnclem3  37216  ftc1cnnc  37235  sdclem2  37285  fdc  37288  istotbnd3  37314  isbnd2  37326  isbnd3  37327  prdsbnd  37336  cntotbnd  37339  heibor1lem  37352  heibor1  37353  heiborlem10  37363  rrncmslem  37375  ghomco  37434  1idl  37569  unichnidl  37574  disjlem18  38341  prtlem10  38406  prtlem18  38418  atlatmstc  38860  cvrexchlem  38961  paddasslem14  39375  pexmidlem5N  39516  cdleme29ex  39916  cdlemefr29exN  39944  cdleme32fva  39979  diarnN  40671  dihlsscpre  40776  isnacs3  42195  fnwe2lem2  42540  kelac1  42552  hbtlem5  42617  hbt  42619  dgraa0p  42638  ofoafg  42848  ofoafo  42850  naddcnffo  42858  fzunt  42950  fzuntd  42951  monoordxrv  44927  rlimdmafv  46620  rlimdmafv2  46701  fmtnoprmfac2  46970  perfectALTVlem2  47125  mogoldbb  47188  lindslinindsimp2  47643