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

This theorem is referenced by:  animpimp2impd  843  3expia  1118  reximddv  3234  rexlimdvaa  3244  disjxiun  5027  wereu2  5516  ordtr3  6204  fcof1  7021  knatar  7089  riota5f  7121  ovmpodf  7285  extmptsuppeq  7837  suppss  7843  suppss2  7847  wfrlem17  7954  smoord  7985  tfrlem9a  8005  oaass  8170  oelimcl  8209  oaabs2  8255  swoso  8305  eceqoveq  8385  domdifsn  8583  domunsncan  8600  omxpenlem  8601  enfixsn  8609  mapdom2  8672  frfi  8747  fofinf1o  8783  finsschain  8815  elfiun  8878  marypha1lem  8881  eqsupd  8905  eqinfd  8933  ordiso2  8963  ordtypelem6  8971  ordtypelem7  8972  ordtypelem10  8975  oismo  8988  wemapsolem  8998  brwdom2  9021  wdomtr  9023  unwdomg  9032  xpwdomg  9033  unxpwdom2  9036  cantnfval2  9116  cantnfle  9118  cantnflem1  9136  cantnf  9140  r1ordg  9191  tcrank  9297  carddomi2  9383  harval2  9410  infxpenlem  9424  infxpenc2lem2  9431  fseqenlem1  9435  dfac8clem  9443  acndom2  9465  infpwfien  9473  iunfictbso  9525  dfac12lem3  9556  infxp  9626  coflim  9672  cofsmo  9680  coftr  9684  sornom  9688  infpssrlem4  9717  enfin2i  9732  fin23lem26  9736  fin23lem27  9739  fin23lem36  9759  fin23lem40  9762  isf32lem5  9768  isf34lem4  9788  isfin1-3  9797  fin1a2lem10  9820  fin1a2lem13  9823  fin1a2s  9825  hsmexlem4  9840  ttukeylem5  9924  ttukeylem6  9925  ttukeylem7  9926  alephval2  9983  gchor  10038  fpwwe2lem7  10047  fpwwe2lem12  10052  fpwwe2  10054  pwfseqlem4a  10072  pwfseqlem4  10073  winalim2  10107  gchina  10110  inar1  10186  nqereq  10346  prlem934  10444  prlem936  10458  addsrmo  10484  mulsrmo  10485  supsrlem  10522  axpre-sup  10580  dedekind  10792  dedekindle  10793  mulge0b  11499  supaddc  11595  supmul1  11597  un0addcl  11918  un0mulcl  11919  uzwo3  12331  qbtwnre  12580  xlemul1a  12669  seqcl2  13384  seqfveq2  13388  seqshft2  13392  monoord  13396  seqsplit  13399  seqf1olem1  13405  seqid2  13412  seqhomo  13413  expnegz  13459  expcan  13529  ltexp2  13530  discr  13597  bcval5  13674  hashbc  13807  hashf1lem2  13810  seqcoll  13818  seqcoll2  13819  wrdind  14075  wrd2ind  14076  cau3lem  14706  ello1d  14872  lo1bdd2  14873  rlimclim  14895  climrlim2  14896  rlimdm  14900  rlimcn1  14937  reccn2  14945  rlimsqzlem  14997  lo1le  15000  caucvgrlem  15021  caurcvg2  15026  summolem2  15065  zsum  15067  fsum  15069  fsumf1o  15072  sumss  15073  fsumss  15074  fsumcl2lem  15080  fsumadd  15088  fsumcom2  15121  fsum0diag2  15130  fsummulc2  15131  fsumconst  15137  fsumrelem  15154  fsumrlim  15158  fsumo1  15159  divrcnv  15199  geomulcvg  15224  mertenslem2  15233  prodmolem2  15281  zprod  15283  fprod  15287  fprodf1o  15292  prodss  15293  fprodss  15294  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodconst  15324  fprodn0  15325  fprodcom2  15330  ruclem8  15582  dvds0lem  15612  dvdsnegb  15619  dvdssub2  15643  bitsf1  15785  bitsshft  15814  bezoutlem3  15879  bezoutlem4  15880  isprm5  16041  isprm6  16048  hashgcdeq  16116  modprminv  16126  modprminveq  16127  reumodprminv  16131  pcqmul  16180  pcqcl  16183  pcxcl  16187  pc2dvds  16205  pcadd  16215  pcmpt  16218  pockthg  16232  infpnlem1  16236  prmreclem5  16246  vdwlem2  16308  vdwlem9  16315  vdwlem10  16316  vdwlem12  16318  ramub  16339  0ram  16346  ramub1lem2  16353  ramub1  16354  ramcl  16355  mreexexd  16911  acsfn2  16926  iscatd  16936  catpropd  16971  setcmon  17339  pleval2i  17566  psss  17816  mgmidsssn0  17874  mhmeql  17982  frmdss2  18020  frmdup3  18024  grprcan  18129  dfgrp3lem  18189  mulgnn0ass  18255  isnsg3  18304  ghmpreima  18372  ghmeql  18373  gaorber  18430  f1omvdco2  18568  psgnunilem1  18613  psgnunilem2  18615  oddvds  18667  gexdvds  18701  sylow1lem1  18715  odcau  18721  pgpssslw  18731  sylow2alem2  18735  sylow2blem3  18739  fislw  18742  lsmmod  18793  efgredlem  18865  frgpup3  18896  gsumval3  19020  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  gsum2d2lem  19086  ablfac1eulem  19187  pgpfac1lem5  19194  ablfaclem3  19202  issubdrg  19553  lss1d  19728  lmhmeql  19820  lspextmo  19821  lspsnat  19910  lsppratlem6  19917  islbs3  19920  lbsextlem4  19926  lidl1el  19984  cnsubrg  20151  gsumfsum  20158  prmirredlem  20186  znidomb  20253  frgpcyg  20265  cssmre  20382  dsmmsubg  20432  dsmmlss  20433  frlmsslsp  20485  lindff1  20509  lindfrn  20510  rnasclassa  20581  mvrf1  20663  mplsubglem  20672  mpllsslem  20673  mplcoe1  20705  mplcoe5  20708  gsummoncoe1  20933  mat1dimcrng  21082  mdetdiaglem  21203  mdetunilem7  21223  mdetunilem8  21224  mdetunilem9  21225  cpmatacl  21321  cpmatmcllem  21323  mp2pm2mplem4  21414  en2top  21590  toponmre  21698  topssnei  21729  innei  21730  clslp  21753  restcls  21786  restntr  21787  ordtrest2lem  21808  cnpco  21872  cncls2  21878  cncnpi  21883  cncnp  21885  cnconst2  21888  cnpdis  21898  lmcnp  21909  cnhaus  21959  isreg2  21982  cncmp  21997  tgcmp  22006  sscmp  22010  cmpfi  22013  cnconn  22027  iunconnlem  22032  clsconn  22035  1stcfb  22050  1stcrest  22058  2ndcctbss  22060  2ndcdisj  22061  1stcelcls  22066  1stccnp  22067  restnlly  22087  cldllycmp  22100  lly1stc  22101  dislly  22102  locfincmp  22131  comppfsc  22137  kgentopon  22143  kgenidm  22152  1stckgenlem  22158  kgencn3  22163  ptpjpre1  22176  ptbasin  22182  txcls  22209  tx2cn  22215  ptpjcn  22216  ptclsg  22220  ptcnp  22227  txdis  22237  txlly  22241  txnlly  22242  pthaus  22243  txtube  22245  txcmplem1  22246  txcmplem2  22247  txcmp  22248  txhaus  22252  txkgen  22257  xkohaus  22258  xkococnlem  22264  xkococn  22265  txconn  22294  qtopeu  22321  qtoprest  22322  regr1lem2  22345  kqreglem1  22346  cmphaushmeo  22405  xkocnv  22419  fgabs  22484  filuni  22490  trufil  22515  ufileu  22524  filufint  22525  fin1aufil  22537  elfm2  22553  rnelfmlem  22557  fmfnfmlem2  22560  fmfnfmlem4  22562  fmufil  22564  flimopn  22580  fbflim2  22582  hausflimi  22585  hausflim  22586  flimcf  22587  flimclslem  22589  flimsncls  22591  hauspwpwf1  22592  cnpflfi  22604  fclsnei  22624  fclscf  22630  flimfnfcls  22633  fclscmp  22635  ufilcmp  22637  fcfnei  22640  cnpfcf  22646  alexsublem  22649  alexsub  22650  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  ptcmplem3  22659  ptcmplem4  22660  ptcmplem5  22661  symgtgp  22711  tgpconncompeqg  22717  tgpconncomp  22718  ghmcnp  22720  tgpt0  22724  qustgplem  22726  haustsms2  22742  tsmsgsum  22744  tsmsres  22749  tsmsxp  22760  imasdsf1olem  22980  xbln0  23021  blssps  23031  blss  23032  neibl  23108  blcld  23112  metss  23115  metequiv2  23117  met1stc  23128  metrest  23131  prdsxmslem2  23136  metcnp3  23147  nrmmetd  23181  nlmvscnlem1  23292  nrginvrcnlem  23297  nmoleub  23337  icccmplem2  23428  icccmp  23430  reconnlem2  23432  xrge0tsms  23439  metdstri  23456  metdseq0  23459  metdscn  23461  cnmpopc  23533  lebnumlem3  23568  pcoval2  23621  pcopt  23627  nmoleub2lem  23719  nmhmcn  23725  ipcnlem1  23849  cfilfcls  23878  cmetcaulem  23892  iscmet3lem2  23896  iscmet3  23897  equivcau  23904  caubl  23912  bcthlem2  23929  bcthlem3  23930  bcthlem4  23931  bcthlem5  23932  ivthlem2  24056  ivthlem3  24057  ovoliunlem2  24107  ovolicc2lem2  24122  ovolicc2lem5  24125  ovolicc2  24126  ismbl2  24131  nulmbl  24139  nulmbl2  24140  unmbl  24141  shftmbl  24142  voliunlem3  24156  volsup  24160  ioombl1lem4  24165  ioombl1  24166  icombl  24168  ioombl  24169  uniioombl  24193  opnmbllem  24205  volivth  24211  vitali  24217  mbflimsup  24270  i1fadd  24299  itg1addlem4  24303  itg2le  24343  itg2seq  24346  itg2lea  24348  itg2splitlem  24352  itg2split  24353  itg2mono  24357  itg2gt0  24364  itg2cnlem2  24366  itgss  24415  itgfsum  24430  itgcn  24448  ellimc3  24482  limcco  24496  limciun  24497  dvnres  24534  dvnfre  24555  rolle  24593  c1liplem1  24599  dvivth  24613  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop  24619  dvcnvrelem1  24620  dvfsumrlim  24634  dvfsum2  24637  ftc1a  24640  ftc1lem6  24644  itgsubst  24652  tdeglem4  24661  mdegaddle  24675  mdegvscale  24676  mdegmullem  24679  deg1tmle  24718  ply1divex  24737  dvdsq1p  24761  fta1g  24768  fta1b  24770  plyco0  24789  coeeulem  24821  dgrlem  24826  plyco  24838  coemullem  24847  dgreq0  24862  dgrco  24872  plydivex  24893  quotcan  24905  aannenlem1  24924  aalioulem2  24929  aalioulem3  24930  taylthlem1  24968  ulmbdd  24993  itgulm  25003  radcnvlt1  25013  psercnlem1  25020  abelthlem2  25027  abelthlem8  25034  logcnlem5  25237  efopn  25249  cxpmul2z  25282  cxpcn3lem  25336  cxpeq  25346  xrlimcnp  25554  cxplim  25557  o1cxp  25560  cxploglim  25563  scvxcvx  25571  jensen  25574  ftalem1  25658  ftalem2  25659  fta  25665  basellem3  25668  isppw2  25700  ppinprm  25737  chtnprm  25739  dvdsmulf1o  25779  chtublem  25795  perfectlem2  25814  dchrfi  25839  dchrptlem1  25848  dchrptlem2  25849  dchrptlem3  25850  dchrsum2  25852  bposlem1  25868  bposlem3  25870  2sqlem5  26006  2sqlem6  26007  2sqlem8  26010  2sqlem10  26012  2sqb  26016  chebbnd1lem1  26053  chtppilimlem2  26058  dchrisum0flb  26094  dchrisum0fno1  26095  dchrisum0  26104  pntrsumbnd2  26151  pntpbnd1  26170  pntpbnd2  26171  pntlemp  26194  pnt3  26196  qabvle  26209  ostth2lem2  26218  ostth3  26222  ostth  26223  colinearalglem4  26703  axcontlem10  26767  upgrex  26885  smcnlem  28480  ubthlem1  28653  ubthlem3  28655  htthlem  28700  5oalem6  29442  leopmuli  29916  pjnormssi  29951  pjclem4  29982  pj3si  29990  hatomistici  30145  sumdmdlem  30201  wrdt2ind  30653  xrge0tsmsd  30742  isarchiofld  30941  ordtrest2NEWlem  31275  qqhf  31337  eulerpartlemb  31736  ballotlemfc0  31860  ballotlemfcc  31861  sgn3da  31909  subfacp1lem5  32544  erdszelem7  32557  erdszelem11  32561  pconnconn  32591  txpconn  32592  connpconn  32595  sconnpi1  32599  txsconn  32601  cvxsconn  32603  cvmopnlem  32638  cvmfolem  32639  cvmliftmolem2  32642  cvmliftlem7  32651  cvmliftlem10  32654  cvmlift2lem10  32672  cvmlift3lem4  32682  cvmlift3lem8  32686  satfun  32771  msubff1  32916  frpomin  33191  wzel  33224  wsuclem  33225  frrlem14  33249  nolt02o  33312  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  noetalem3  33332  btwnouttr2  33596  cgrxfr  33629  btwnxfr  33630  brcolinear  33633  lineext  33650  btwnconn1lem13  33673  midofsegid  33678  segcon2  33679  brsegle  33682  seglecgr12im  33684  segletr  33688  colinbtwnle  33692  broutsideof2  33696  btwnoutside  33699  broutsideof3  33700  outsideoftr  33703  outsideofeq  33704  outsideofeu  33705  outsidele  33706  lineunray  33721  lineelsb2  33722  linethru  33727  finminlem  33779  nn0prpwlem  33783  neibastop2lem  33821  neibastop2  33822  neibastop3  33823  topjoin  33826  tailfb  33838  relowlssretop  34780  fvineqsneq  34829  wl-sbcom2d-lem1  34960  finixpnum  35042  poimirlem6  35063  poimirlem7  35064  poimirlem13  35070  poimirlem26  35083  poimirlem29  35086  heicant  35092  opnmbllem0  35093  mblfinlem3  35096  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  itg2addnclem  35108  itg2addnclem3  35110  ftc1cnnc  35129  sdclem2  35180  fdc  35183  istotbnd3  35209  isbnd2  35221  isbnd3  35222  prdsbnd  35231  cntotbnd  35234  heibor1lem  35247  heibor1  35248  heiborlem10  35258  rrncmslem  35270  ghomco  35329  1idl  35464  unichnidl  35469  prtlem10  36161  prtlem18  36173  atlatmstc  36615  cvrexchlem  36715  paddasslem14  37129  pexmidlem5N  37270  cdleme29ex  37670  cdlemefr29exN  37698  cdleme32fva  37733  diarnN  38425  dihlsscpre  38530  isnacs3  39651  fnwe2lem2  39995  kelac1  40007  hbtlem5  40072  hbt  40074  dgraa0p  40093  monoordxrv  42121  rlimdmafv  43733  rlimdmafv2  43814  fmtnoprmfac2  44084  perfectALTVlem2  44240  mogoldbb  44303  mgmhmeql  44423  lindslinindsimp2  44872