Theorem expr 460

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  animpimp2impd  857  3expia  1135  rexlimdvaa  3165  reximddv  3179  disjxiun  5098  wereu2  5645  frpomin  6328  ordtr3  6393  fcof1  7272  knatar  7342  riota5f  7382  ovmpodf  7553  extmptsuppeq  8169  suppss  8175  suppss2  8181  frrlem14  8281  fprresex  8292  smoord  8337  tfrlem9a  8358  oaass  8531  oelimcl  8571  oaabs2  8620  cofon1  8643  naddssim  8657  swoso  8714  eceqoveq  8805  domdifsn  9033  domunsncan  9050  omxpenlem  9051  enfixsn  9059  mapdom2  9121  frfi  9230  fofinf1o  9276  finsschain  9303  elfiun  9377  marypha1lem  9380  eqsupd  9404  eqinfd  9433  ordiso2  9464  ordtypelem6  9472  ordtypelem7  9473  ordtypelem10  9476  oismo  9489  wemapsolem  9499  brwdom2  9522  wdomtr  9524  unwdomg  9533  xpwdomg  9534  unxpwdom2  9537  cantnfval2  9625  cantnfle  9627  cantnflem1  9645  cantnf  9649  r1ordg  9737  tcrank  9843  carddomi2  9929  harval2  9956  infxpenlem  9970  infxpenc2lem2  9977  fseqenlem1  9981  dfac8clem  9989  acndom2  10011  infpwfien  10019  iunfictbso  10071  dfac12lem3  10103  infxp  10171  coflim  10219  cofsmo  10227  coftr  10231  sornom  10235  infpssrlem4  10264  enfin2i  10279  fin23lem26  10283  fin23lem27  10286  fin23lem36  10306  fin23lem40  10309  isf32lem5  10315  isf34lem4  10335  isfin1-3  10344  fin1a2lem10  10367  fin1a2lem13  10370  fin1a2s  10372  hsmexlem4  10387  ttukeylem5  10471  ttukeylem6  10472  ttukeylem7  10473  alephval2  10531  gchor  10586  fpwwe2lem6  10595  fpwwe2lem11  10600  fpwwe2  10602  pwfseqlem4a  10620  pwfseqlem4  10621  winalim2  10655  gchina  10658  inar1  10734  nqereq  10894  prlem934  10992  prlem936  11006  addsrmo  11032  mulsrmo  11033  supsrlem  11070  axpre-sup  11128  dedekind  11347  dedekindle  11348  mulge0b  12063  supaddc  12160  supmul1  12162  un0addcl  12515  un0mulcl  12516  uzwo3  12945  qbtwnre  13203  xlemul1a  13292  seqcl2  14034  seqfveq2  14038  seqshft2  14042  monoord  14046  seqsplit  14049  seqf1olem1  14055  seqid2  14062  seqhomo  14063  expnegz  14110  expcan  14183  ltexp2  14184  discr  14254  bcval5  14332  hashbc  14467  hashf1lem2  14470  seqcoll  14478  seqcoll2  14479  wrdind  14736  wrd2ind  14737  sgn3da  15115  cau3lem  15383  ello1d  15551  lo1bdd2  15552  rlimclim  15574  climrlim2  15575  rlimdm  15579  rlimcn1  15616  reccn2  15625  rlimsqzlem  15677  lo1le  15680  caucvgrlem  15701  caurcvg2  15706  summolem2  15744  zsum  15746  fsum  15748  fsumf1o  15751  sumss  15752  fsumss  15753  fsumcl2lem  15759  fsumadd  15768  fsumcom2  15802  fsum0diag2  15811  fsummulc2  15812  fsumconst  15818  fsumrelem  15836  fsumrlim  15840  fsumo1  15841  divrcnv  15883  geomulcvg  15907  mertenslem2  15916  prodmolem2  15966  zprod  15968  fprod  15972  fprodf1o  15977  prodss  15978  fprodss  15979  fprodcl2lem  15981  fprodmul  15991  fproddiv  15992  fprodconst  16009  fprodn0  16010  fprodcom2  16015  ruclem8  16270  dvds0lem  16301  dvdsnegb  16308  dvdssub2  16336  bitsf1  16481  bitsshft  16510  bezoutlem3  16576  bezoutlem4  16577  isprm5  16743  isprm6  16750  hashgcdeq  16826  modprminv  16836  modprminveq  16837  reumodprminv  16841  pcqmul  16890  pcqcl  16893  pcxnn0cl  16897  pcxcl  16898  pc2dvds  16916  pcadd  16926  pcmpt  16929  pockthg  16943  infpnlem1  16947  prmreclem5  16957  vdwlem2  17019  vdwlem9  17026  vdwlem10  17027  vdwlem12  17029  ramub  17050  0ram  17057  ramub1lem2  17064  ramub1  17065  ramcl  17066  mreexexd  17681  acsfn2  17696  iscatd  17706  catpropd  17742  setcmon  18121  pleval2i  18367  psss  18613  mgmidsssn0  18707  mgmhmeql  18751  mhmeql  18861  frmdss2  18898  frmdup3  18902  grprcan  19016  dfgrp3lem  19081  mulgnn0ass  19153  isnsg3  19202  ghmpreima  19279  ghmeql  19280  gaorber  19349  f1omvdco2  19489  psgnunilem1  19534  psgnunilem2  19536  oddvds  19588  gexdvds  19625  sylow1lem1  19639  odcau  19645  pgpssslw  19655  sylow2alem2  19659  sylow2blem3  19663  fislw  19666  lsmmod  19716  efgredlem  19788  frgpup3  19819  gsumval3  19948  gsumzres  19950  gsumzcl2  19951  gsumzf1o  19953  gsumzaddlem  19962  gsumconst  19975  gsumzmhm  19978  gsumzoppg  19985  gsum2d2lem  20014  ablfac1eulem  20115  pgpfac1lem5  20122  ablfaclem3  20130  issubdrg  20830  lss1d  21031  lmhmeql  21123  lspextmo  21124  lspsnat  21216  lsppratlem6  21223  islbs3  21226  lbsextlem4  21232  lidl1el  21297  cnsubrg  21480  gsumfsum  21487  prmirredlem  21525  znidomb  21614  frgpcyg  21626  cssmre  21746  dsmmsubg  21796  dsmmlss  21797  frlmsslsp  21849  lindff1  21873  lindfrn  21874  rnasclassa  21948  mvrf1  22038  mplsubglem  22051  mpllsslem  22052  mplcoe1  22091  mplcoe5  22094  gsummoncoe1  22372  mat1dimcrng  22538  mdetdiaglem  22659  mdetunilem7  22679  mdetunilem8  22680  mdetunilem9  22681  cpmatacl  22777  cpmatmcllem  22779  mp2pm2mplem4  22870  en2top  23046  toponmre  23154  topssnei  23185  innei  23186  clslp  23209  restcls  23242  restntr  23243  ordtrest2lem  23264  cnpco  23328  cncls2  23334  cncnpi  23339  cncnp  23341  cnconst2  23344  cnpdis  23354  lmcnp  23365  cnhaus  23415  isreg2  23438  cncmp  23453  tgcmp  23462  sscmp  23466  cmpfi  23469  cnconn  23483  iunconnlem  23488  clsconn  23491  1stcfb  23506  1stcrest  23514  2ndcctbss  23516  2ndcdisj  23517  1stcelcls  23522  1stccnp  23523  restnlly  23543  cldllycmp  23556  lly1stc  23557  dislly  23558  locfincmp  23587  comppfsc  23593  kgentopon  23599  kgenidm  23608  1stckgenlem  23614  kgencn3  23619  ptpjpre1  23632  ptbasin  23638  txcls  23665  tx2cn  23671  ptpjcn  23672  ptclsg  23676  ptcnp  23683  txdis  23693  txlly  23697  txnlly  23698  pthaus  23699  txtube  23701  txcmplem1  23702  txcmplem2  23703  txcmp  23704  txhaus  23708  txkgen  23713  xkohaus  23714  xkococnlem  23720  xkococn  23721  txconn  23750  qtopeu  23777  qtoprest  23778  regr1lem2  23801  kqreglem1  23802  cmphaushmeo  23861  xkocnv  23875  fgabs  23940  filuni  23946  trufil  23971  ufileu  23980  filufint  23981  fin1aufil  23993  elfm2  24009  rnelfmlem  24013  fmfnfmlem2  24016  fmfnfmlem4  24018  fmufil  24020  flimopn  24036  fbflim2  24038  hausflimi  24041  hausflim  24042  flimcf  24043  flimclslem  24045  flimsncls  24047  hauspwpwf1  24048  cnpflfi  24060  fclsnei  24080  fclscf  24086  flimfnfcls  24089  fclscmp  24091  ufilcmp  24093  fcfnei  24096  cnpfcf  24102  alexsublem  24105  alexsub  24106  alexsubALTlem2  24109  alexsubALTlem3  24110  alexsubALTlem4  24111  ptcmplem3  24115  ptcmplem4  24116  ptcmplem5  24117  symgtgp  24167  tgpconncompeqg  24173  tgpconncomp  24174  ghmcnp  24176  tgpt0  24180  qustgplem  24182  haustsms2  24198  tsmsgsum  24200  tsmsres  24205  tsmsxp  24216  imasdsf1olem  24434  xbln0  24475  blssps  24485  blss  24486  neibl  24562  blcld  24566  metss  24569  metequiv2  24571  met1stc  24582  metrest  24585  prdsxmslem2  24590  metcnp3  24601  nrmmetd  24635  nlmvscnlem1  24747  nrginvrcnlem  24752  nmoleub  24792  icccmplem2  24885  icccmp  24887  reconnlem2  24889  xrge0tsms  24896  metdstri  24913  metdseq0  24916  metdscn  24918  cnmpopc  24991  lebnumlem3  25026  pcoval2  25079  pcopt  25085  nmoleub2lem  25177  nmhmcn  25183  ipcnlem1  25308  cfilfcls  25337  cmetcaulem  25351  iscmet3lem2  25355  iscmet3  25356  equivcau  25363  caubl  25371  bcthlem2  25388  bcthlem3  25389  bcthlem4  25390  bcthlem5  25391  ivthlem2  25515  ivthlem3  25516  ovoliunlem2  25566  ovolicc2lem2  25581  ovolicc2lem5  25584  ovolicc2  25585  ismbl2  25590  nulmbl  25598  nulmbl2  25599  unmbl  25600  shftmbl  25601  voliunlem3  25615  volsup  25619  ioombl1lem4  25624  ioombl1  25625  icombl  25627  ioombl  25628  uniioombl  25652  opnmbllem  25664  volivth  25670  vitali  25676  mbflimsup  25729  i1fadd  25758  itg1addlem4  25762  itg2le  25802  itg2seq  25805  itg2lea  25807  itg2splitlem  25811  itg2split  25812  itg2mono  25816  itg2gt0  25823  itg2cnlem2  25825  itgss  25875  itgfsum  25890  itgcn  25908  ellimc3  25942  limcco  25956  limciun  25957  dvnres  25994  dvnfre  26015  rolle  26053  c1liplem1  26059  dvivth  26073  dvne0  26074  lhop1lem  26076  lhop1  26077  lhop  26079  dvcnvrelem1  26080  dvfsumrlim  26094  dvfsum2  26097  ftc1a  26100  ftc1lem6  26104  itgsubst  26112  tdeglem4  26121  mdegaddle  26135  mdegvscale  26136  mdegmullem  26139  deg1tmle  26179  ply1divex  26198  dvdsq1p  26224  fta1g  26231  fta1b  26233  plyco0  26253  coeeulem  26285  dgrlem  26290  plyco  26302  coemullem  26311  dgreq0  26326  dgrco  26336  plydivex  26362  quotcan  26374  aannenlem1  26393  aalioulem2  26398  aalioulem3  26399  taylthlem1  26437  ulmbdd  26462  itgulm  26472  radcnvlt1  26482  psercnlem1  26489  abelthlem2  26496  abelthlem8  26503  logcnlem5  26712  efopn  26724  cxpmul2z  26757  cxpcn3lem  26813  cxpeq  26823  xrlimcnp  27034  cxplim  27037  o1cxp  27040  cxploglim  27043  scvxcvx  27051  jensen  27054  ftalem1  27138  ftalem2  27139  fta  27145  basellem3  27148  isppw2  27180  ppinprm  27217  chtnprm  27219  mpodvdsmulf1o  27259  dvdsmulf1o  27261  chtublem  27276  perfectlem2  27295  dchrfi  27320  dchrptlem1  27329  dchrptlem2  27330  dchrptlem3  27331  dchrsum2  27333  bposlem1  27349  bposlem3  27351  2sqlem5  27487  2sqlem6  27488  2sqlem8  27491  2sqlem10  27493  2sqb  27497  chebbnd1lem1  27534  chtppilimlem2  27539  dchrisum0flb  27575  dchrisum0fno1  27576  dchrisum0  27585  pntrsumbnd2  27632  pntpbnd1  27651  pntpbnd2  27652  pntlemp  27675  pnt3  27677  qabvle  27690  ostth2lem2  27699  ostth3  27703  ostth  27704  nolt02o  27760  nogt01o  27761  nosupprefixmo  27765  noinfprefixmo  27766  nosupbnd1lem3  27775  nosupbnd1lem4  27776  nosupbnd1lem5  27777  noinfbnd1lem3  27790  noinfbnd1lem4  27791  noinfbnd1lem5  27792  noetasuplem4  27801  noetainflem4  27805  etaslts  27887  cuteq1  27911  madebdaylemlrcut  27993  cutlt  28026  mulsuniflem  28243  bdayons  28370  addonbday  28373  om2noseqlt  28393  n0fincut  28449  bdaypw2n0bndlem  28557  bdayfinbndlem1  28561  z12sge0  28577  readdscl  28593  remulscl  28596  colinearalglem4  29111  axcontlem10  29175  upgrex  29294  smcnlem  30901  ubthlem1  31074  ubthlem3  31076  htthlem  31121  5oalem6  31863  leopmuli  32337  pjnormssi  32372  pjclem4  32403  pj3si  32411  hatomistici  32566  sumdmdlem  32622  wrdt2ind  33132  xrge0tsmsd  33254  isarchiofld  33380  ordtrest2NEWlem  34220  qqhf  34284  eulerpartlemb  34666  ballotlemfc0  34791  ballotlemfcc  34792  subfacp1lem5  35535  erdszelem7  35548  erdszelem11  35552  pconnconn  35582  txpconn  35583  connpconn  35586  sconnpi1  35590  txsconn  35592  cvxsconn  35594  cvmopnlem  35629  cvmfolem  35630  cvmliftmolem2  35633  cvmliftlem7  35642  cvmliftlem10  35645  cvmlift2lem10  35663  cvmlift3lem4  35673  cvmlift3lem8  35677  satfun  35762  msubff1  35907  wzel  36173  wsuclem  36174  btwnouttr2  36373  cgrxfr  36406  btwnxfr  36407  brcolinear  36410  lineext  36427  btwnconn1lem13  36450  midofsegid  36455  segcon2  36456  brsegle  36459  seglecgr12im  36461  segletr  36465  colinbtwnle  36469  broutsideof2  36473  btwnoutside  36476  broutsideof3  36477  outsideoftr  36480  outsideofeq  36481  outsideofeu  36482  outsidele  36483  lineunray  36498  lineelsb2  36499  linethru  36504  finminlem  36679  nn0prpwlem  36683  neibastop2lem  36721  neibastop2  36722  neibastop3  36723  topjoin  36726  tailfb  36738  axtcond  36839  relowlssretop  37858  fvineqsneq  37907  wl-sbcom2d-lem1  38063  finixpnum  38105  poimirlem6  38126  poimirlem7  38127  poimirlem13  38133  poimirlem26  38146  poimirlem29  38149  heicant  38155  opnmbllem0  38156  mblfinlem3  38159  ismblfin  38161  ovoliunnfl  38162  voliunnfl  38164  volsupnfl  38165  itg2addnclem  38171  itg2addnclem3  38173  ftc1cnnc  38192  sdclem2  38242  fdc  38245  istotbnd3  38271  isbnd2  38283  isbnd3  38284  prdsbnd  38293  cntotbnd  38296  heibor1lem  38309  heibor1  38310  heiborlem10  38320  rrncmslem  38332  ghomco  38391  1idl  38526  unichnidl  38531  disjlem18  39403  prtlem10  39490  prtlem18  39502  atlatmstc  39944  cvrexchlem  40044  paddasslem14  40458  pexmidlem5N  40599  cdleme29ex  40999  cdlemefr29exN  41027  cdleme32fva  41062  diarnN  41754  dihlsscpre  41859  isnacs3  43292  fnwe2lem2  43629  kelac1  43641  hbtlem5  43706  hbt  43708  dgraa0p  43727  ofoafg  43932  ofoafo  43934  naddcnffo  43942  fzunt  44032  fzuntd  44033  monoordxrv  46056  rlimdmafv  47772  rlimdmafv2  47853  fmtnoprmfac2  48177  perfectALTVlem2  48345  mogoldbb  48408  lindslinindsimp2  49086