Theorem expr 462

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  animpimp2impd  860  3expia  1139  rexlimdvaa  3165  reximddv  3179  disjxiun  5100  wereu2  5648  frpomin  6343  ordtr3  6409  fcof1  7295  knatar  7367  riota5f  7405  ovmpodf  7576  fnwe2lem3  8147  extmptsuppeq  8205  suppss  8211  suppss2  8217  frrlem14  8317  fprresex  8328  smoord  8373  tfrlem9a  8394  oaass  8569  oelimcl  8609  oaabs2  8658  cofon1  8681  naddssim  8695  swoso  8752  eceqoveq  8843  domdifsn  9079  domunsncan  9096  omxpenlem  9097  enfixsn  9105  mapdom2  9167  frfi  9276  fofinf1o  9321  finsschain  9348  elfiun  9422  marypha1lem  9425  eqsupd  9449  eqinfd  9478  ordiso2  9509  ordtypelem6  9517  ordtypelem7  9518  ordtypelem10  9521  oismo  9534  wemapsolem  9544  brwdom2  9567  wdomtr  9569  unwdomg  9578  xpwdomg  9579  unxpwdom2  9582  cantnfval2  9670  cantnfle  9672  cantnflem1  9690  cantnf  9694  r1ordg  9785  tcrank  9901  carddomi2  10051  harval2  10078  infxpenlem  10092  infxpenc2lem2  10099  fseqenlem1  10103  dfac8clem  10111  acndom2  10133  infpwfien  10141  iunfictbso  10193  dfac12lem3  10224  infxp  10292  coflim  10339  cofsmo  10347  coftr  10351  sornom  10355  infpssrlem4  10384  enfin2i  10399  fin23lem26  10403  fin23lem27  10406  fin23lem36  10426  fin23lem40  10429  isf32lem5  10435  isf34lem4  10455  isfin1-3  10464  fin1a2lem10  10487  fin1a2lem13  10490  fin1a2s  10492  hsmexlem4  10507  ttukeylem5  10591  ttukeylem6  10592  ttukeylem7  10593  alephval2  10657  gchor  10712  fpwwe2lem6  10721  fpwwe2lem11  10726  fpwwe2  10728  pwfseqlem4a  10746  pwfseqlem4  10747  winalim2  10781  gchina  10784  inar1  10860  nqereq  11020  prlem934  11118  prlem936  11132  addsrmo  11158  mulsrmo  11159  supsrlem  11196  axpre-sup  11254  dedekind  11473  dedekindle  11474  mulge0b  12187  supaddc  12284  supmul1  12286  un0addcl  12639  un0mulcl  12640  uzwo3  13070  qbtwnre  13329  xlemul1a  13418  seqcl2  14163  seqfveq2  14167  seqshft2  14171  monoord  14175  seqsplit  14178  seqf1olem1  14184  seqid2  14191  seqhomo  14192  expnegz  14239  expcan  14312  ltexp2  14313  discr  14384  bcval5  14462  hashbc  14598  hashf1lem2  14601  seqcoll  14609  seqcoll2  14610  wrdind  14871  wrd2ind  14872  sgn3da  15254  cau3lem  15522  ello1d  15690  lo1bdd2  15691  rlimclim  15713  climrlim2  15714  rlimdm  15718  rlimcn1  15755  reccn2  15764  rlimsqzlem  15816  lo1le  15819  caucvgrlem  15840  caurcvg2  15845  summolem2  15882  zsum  15884  fsum  15886  fsumf1o  15889  sumss  15890  fsumss  15891  fsumcl2lem  15897  fsumadd  15906  fsumcom2  15940  fsum0diag2  15949  fsummulc2  15950  fsumconst  15956  fsumrelem  15974  fsumrlim  15978  fsumo1  15979  divrcnv  16021  geomulcvg  16045  mertenslem2  16054  prodmolem2  16102  zprod  16104  fprod  16108  fprodf1o  16113  prodss  16114  fprodss  16115  fprodcl2lem  16117  fprodmul  16127  fproddiv  16128  fprodconst  16145  fprodn0  16146  fprodcom2  16151  ruclem8  16405  dvds0lem  16436  dvdsnegb  16443  dvdssub2  16471  bitsf1  16616  bitsshft  16645  bezoutlem3  16714  bezoutlem4  16715  isprm5  16883  isprm6  16890  hashgcdeq  16967  modprminv  16977  modprminveq  16978  reumodprminv  16982  pcqmul  17031  pcqcl  17034  pcxnn0cl  17038  pcxcl  17039  pc2dvds  17057  pcadd  17067  pcmpt  17070  pockthg  17084  infpnlem1  17088  prmreclem5  17098  vdwlem2  17160  vdwlem9  17167  vdwlem10  17168  vdwlem12  17170  ramub  17191  0ram  17198  ramub1lem2  17205  ramub1  17206  ramcl  17207  mreexexd  17822  acsfn2  17837  iscatd  17847  catpropd  17883  setcmon  18262  pleval2i  18508  psss  18754  mgmidsssn0  18853  mgmhmeql  18905  mhmeql  19022  frmdss2  19059  frmdup3  19063  grprcan  19184  dfgrp3lem  19248  mulgnn0ass  19320  isnsg3  19370  ghmpreima  19452  ghmeql  19453  gaorber  19522  f1omvdco2  19662  psgnunilem1  19707  psgnunilem2  19709  oddvds  19761  gexdvds  19798  sylow1lem1  19812  odcau  19818  pgpssslw  19828  sylow2alem2  19832  sylow2blem3  19836  fislw  19839  lsmmod  19889  efgredlem  19961  frgpup3  19992  gsumval3  20121  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  gsum2d2lem  20187  ablfac1eulem  20288  pgpfac1lem5  20295  ablfaclem3  20303  issubdrg  21037  lss1d  21238  lmhmeql  21330  lspextmo  21331  lspsnat  21423  lsppratlem6  21430  islbs3  21433  lbsextlem4  21439  lidl1el  21505  cnsubrg  21733  gsumfsum  21740  prmirredlem  21778  znidomb  21867  frgpcyg  21879  cssmre  21999  dsmmsubg  22049  dsmmlss  22050  frlmsslsp  22102  lindff1  22126  lindfrn  22127  rnasclassa  22203  mvrf1  22293  mplsubglem  22306  mpllsslem  22307  mplcoe1  22346  mplcoe5  22349  gsummoncoe1  22626  mat1dimcrng  22792  mdetdiaglem  22913  mdetunilem7  22933  mdetunilem8  22934  mdetunilem9  22935  cpmatacl  23034  cpmatmcllem  23036  mp2pm2mplem4  23127  en2top  23303  toponmre  23411  topssnei  23442  innei  23443  clslp  23466  restcls  23499  restntr  23500  ordtrest2lem  23521  cnpco  23585  cncls2  23591  cncnpi  23596  cncnp  23598  cnconst2  23601  cnpdis  23611  lmcnp  23622  cnhaus  23672  isreg2  23695  cncmp  23710  tgcmp  23719  sscmp  23723  cmpfi  23726  cnconn  23740  iunconnlem  23745  clsconn  23748  1stcfb  23763  1stcrest  23771  2ndcctbss  23774  2ndcdisj  23775  1stcelcls  23780  1stccnp  23781  restnlly  23801  cldllycmp  23814  lly1stc  23815  dislly  23816  locfincmp  23845  comppfsc  23851  kgentopon  23857  kgenidm  23866  1stckgenlem  23872  kgencn3  23877  ptpjpre1  23890  ptbasin  23896  txcls  23923  tx2cn  23929  ptpjcn  23930  ptclsg  23934  ptcnp  23941  txdis  23951  txlly  23955  txnlly  23956  pthaus  23957  txtube  23959  txcmplem1  23960  txcmplem2  23961  txcmp  23962  txhaus  23966  txkgen  23971  xkohaus  23972  xkococnlem  23978  xkococn  23979  txconn  24008  qtopeu  24035  qtoprest  24036  regr1lem2  24059  kqreglem1  24060  cmphaushmeo  24119  xkocnv  24133  fgabs  24198  filuni  24204  trufil  24229  ufileu  24238  filufint  24239  fin1aufil  24251  elfm2  24267  rnelfmlem  24271  fmfnfmlem2  24274  fmfnfmlem4  24276  fmufil  24278  flimopn  24294  fbflim2  24296  hausflimi  24299  hausflim  24300  flimcf  24301  flimclslem  24303  flimsncls  24305  hauspwpwf1  24306  cnpflfi  24318  fclsnei  24338  fclscf  24344  flimfnfcls  24347  fclscmp  24349  ufilcmp  24351  fcfnei  24354  cnpfcf  24360  alexsublem  24363  alexsub  24364  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem3  24373  ptcmplem4  24374  ptcmplem5  24375  symgtgp  24425  tgpconncompeqg  24431  tgpconncomp  24432  ghmcnp  24434  tgpt0  24438  qustgplem  24440  haustsms2  24456  tsmsgsum  24458  tsmsres  24463  tsmsxp  24474  imasdsf1olem  24692  xbln0  24733  blssps  24743  blss  24744  neibl  24820  blcld  24824  metss  24827  metequiv2  24829  met1stc  24840  metrest  24843  prdsxmslem2  24848  metcnp3  24859  nrmmetd  24893  nlmvscnlem1  25005  nrginvrcnlem  25010  nmoleub  25050  icccmplem2  25143  icccmp  25145  reconnlem2  25147  xrge0tsms  25154  metdstri  25171  metdseq0  25174  metdscn  25176  cnmpopc  25249  lebnumlem3  25284  pcoval2  25337  pcopt  25343  nmoleub2lem  25435  nmhmcn  25441  ipcnlem1  25566  cfilfcls  25595  cmetcaulem  25609  iscmet3lem2  25613  iscmet3  25614  equivcau  25621  caubl  25629  bcthlem2  25646  bcthlem3  25647  bcthlem4  25648  bcthlem5  25649  ivthlem2  25773  ivthlem3  25774  ovoliunlem2  25824  ovolicc2lem2  25839  ovolicc2lem5  25842  ovolicc2  25843  ismbl2  25848  nulmbl  25856  nulmbl2  25857  unmbl  25858  shftmbl  25859  voliunlem3  25873  volsup  25877  ioombl1lem4  25882  ioombl1  25883  icombl  25885  ioombl  25886  uniioombl  25910  opnmbllem  25922  volivth  25928  vitali  25934  mbflimsup  25987  i1fadd  26016  itg1addlem4  26020  itg2le  26060  itg2seq  26063  itg2lea  26065  itg2splitlem  26069  itg2split  26070  itg2mono  26074  itg2gt0  26081  itg2cnlem2  26083  itgss  26132  itgfsum  26147  itgcn  26165  ellimc3  26199  limcco  26213  limciun  26214  dvnres  26251  dvnfre  26272  rolle  26310  c1liplem1  26316  dvivth  26330  dvne0  26331  lhop1lem  26333  lhop1  26334  lhop  26336  dvcnvrelem1  26337  dvfsumrlim  26351  dvfsum2  26354  ftc1a  26357  ftc1lem6  26361  itgsubst  26369  tdeglem4  26378  mdegaddle  26392  mdegvscale  26393  mdegmullem  26396  deg1tmle  26436  ply1divex  26455  dvdsq1p  26481  fta1g  26488  fta1b  26490  plyco0  26510  coeeulem  26543  dgrlem  26548  plyco  26560  coemullem  26569  dgreq0  26584  dgrco  26594  plydivex  26618  quotcan  26632  aannenlem1  26655  aalioulem2  26660  aalioulem3  26661  taylthlem1  26700  ulmbdd  26725  itgulm  26735  radcnvlt1  26745  psercnlem1  26752  abelthlem2  26759  abelthlem8  26766  logcnlem5  26974  efopn  26986  cxpmul2z  27019  cxpcn3lem  27075  cxpeq  27085  xrlimcnp  27296  cxplim  27299  o1cxp  27302  cxploglim  27305  scvxcvx  27313  jensen  27316  ftalem1  27400  ftalem2  27401  fta  27407  basellem3  27410  isppw2  27442  ppinprm  27479  chtnprm  27481  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chtublem  27538  perfectlem2  27557  dchrfi  27582  dchrptlem1  27591  dchrptlem2  27592  dchrptlem3  27593  dchrsum2  27595  bposlem1  27611  bposlem3  27613  2sqlem5  27749  2sqlem6  27750  2sqlem8  27753  2sqlem10  27755  2sqb  27759  chebbnd1lem1  27796  chtppilimlem2  27801  dchrisum0flb  27837  dchrisum0fno1  27838  dchrisum0  27847  pntrsumbnd2  27894  pntpbnd1  27913  pntpbnd2  27914  pntlemp  27937  pnt3  27939  qabvle  27952  ostth2lem2  27961  ostth3  27965  ostth  27966  nolt02o  28052  nogt01o  28053  nosupprefixmo  28057  noinfprefixmo  28058  nosupbnd1lem3  28067  nosupbnd1lem4  28068  nosupbnd1lem5  28069  noinfbnd1lem3  28082  noinfbnd1lem4  28083  noinfbnd1lem5  28084  noetasuplem4  28093  noetainflem4  28097  etaslts  28179  cuteq1  28203  madebdaylemlrcut  28285  cutlt  28318  mulsuniflem  28535  bdayons  28662  addonbday  28665  om2noseqlt  28685  n0fincut  28741  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  z12sge0  28869  readdscl  28885  remulscl  28888  colinearalglem4  29487  axcontlem10  29551  upgrex  29670  smcnlem  31299  ubthlem1  31472  ubthlem3  31474  htthlem  31519  5oalem6  32261  leopmuli  32735  pjnormssi  32770  pjclem4  32801  pj3si  32809  hatomistici  32964  sumdmdlem  33020  wrdt2ind  33516  xrge0tsmsd  33634  isarchiofld  33760  ordtrest2NEWlem  34554  qqhf  34618  eulerpartlemb  35000  ballotlemfc0  35125  ballotlemfcc  35126  soinfdom  35717  subfacp1lem5  35949  erdszelem7  35962  erdszelem11  35966  pconnconn  35996  txpconn  35997  connpconn  36000  sconnpi1  36004  txsconn  36006  cvxsconn  36008  cvmopnlem  36043  cvmfolem  36044  cvmliftmolem2  36047  cvmliftlem7  36056  cvmliftlem10  36059  cvmlift2lem10  36077  cvmlift3lem4  36087  cvmlift3lem8  36091  satfun  36176  msubff1  36321  wzel  36586  wsuclem  36587  btwnouttr2  36787  cgrxfr  36820  btwnxfr  36821  brcolinear  36824  lineext  36841  btwnconn1lem13  36864  midofsegid  36869  segcon2  36870  brsegle  36873  seglecgr12im  36875  segletr  36879  colinbtwnle  36883  broutsideof2  36887  btwnoutside  36890  broutsideof3  36891  outsideoftr  36894  outsideofeq  36895  outsideofeu  36896  outsidele  36897  lineunray  36912  lineelsb2  36913  linethru  36918  nmulrid  36946  nmuladdss  36962  nadddilem1  36969  finminlem  37106  nn0prpwlem  37110  neibastop2lem  37148  neibastop2  37149  neibastop3  37150  topjoin  37153  tailfb  37165  axtcond  37266  relowlssretop  38286  fvineqsneq  38335  wl-sbcom2d-lem1  38491  finixpnum  38528  poimirlem6  38544  poimirlem7  38545  poimirlem13  38551  poimirlem26  38564  poimirlem29  38567  heicant  38573  opnmbllem0  38574  mblfinlem3  38577  ismblfin  38579  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  itg2addnclem  38589  itg2addnclem3  38591  ftc1cnnc  38610  sdclem2  38676  fdc  38679  istotbnd3  38705  isbnd2  38717  isbnd3  38718  prdsbnd  38727  cntotbnd  38730  heibor1lem  38743  heibor1  38744  heiborlem10  38754  rrncmslem  38766  ghomco  38825  1idl  38960  unichnidl  38965  disjlem18  39835  prtlem10  39922  prtlem18  39934  atlatmstc  40376  cvrexchlem  40476  paddasslem14  40890  pexmidlem5N  41031  cdleme29ex  41431  cdlemefr29exN  41459  cdleme32fva  41494  diarnN  42186  dihlsscpre  42291  isnacs3  43720  kelac1  44064  hbtlem5  44129  hbt  44131  dgraa0p  44150  ofoafg  44355  ofoafo  44357  naddcnffo  44365  fzunt  44455  fzuntd  44456  cocanss2  45921  monoordxrv  46490  rlimdmafv  48246  rlimdmafv2  48327  fmtnoprmfac2  48651  perfectALTVlem2  48819  mogoldbb  48882  lindslinindsimp2  49574