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  5083  wereu2  5623  frpomin  6300  ordtr3  6365  fcof1  7237  knatar  7307  riota5f  7347  ovmpodf  7518  extmptsuppeq  8133  suppss  8139  suppss2  8145  frrlem14  8244  fprresex  8255  smoord  8300  tfrlem9a  8320  oaass  8491  oelimcl  8531  oaabs2  8580  cofon1  8603  naddssim  8616  swoso  8673  eceqoveq  8764  domdifsn  8993  domunsncan  9010  omxpenlem  9011  enfixsn  9019  mapdom2  9081  frfi  9190  fofinf1o  9237  finsschain  9264  elfiun  9338  marypha1lem  9341  eqsupd  9365  eqinfd  9394  ordiso2  9425  ordtypelem6  9433  ordtypelem7  9434  ordtypelem10  9437  oismo  9450  wemapsolem  9460  brwdom2  9483  wdomtr  9485  unwdomg  9494  xpwdomg  9495  unxpwdom2  9498  cantnfval2  9585  cantnfle  9587  cantnflem1  9605  cantnf  9609  r1ordg  9697  tcrank  9803  carddomi2  9889  harval2  9916  infxpenlem  9930  infxpenc2lem2  9937  fseqenlem1  9941  dfac8clem  9949  acndom2  9971  infpwfien  9979  iunfictbso  10031  dfac12lem3  10063  infxp  10131  coflim  10178  cofsmo  10186  coftr  10190  sornom  10194  infpssrlem4  10223  enfin2i  10238  fin23lem26  10242  fin23lem27  10245  fin23lem36  10265  fin23lem40  10268  isf32lem5  10274  isf34lem4  10294  isfin1-3  10303  fin1a2lem10  10326  fin1a2lem13  10329  fin1a2s  10331  hsmexlem4  10346  ttukeylem5  10430  ttukeylem6  10431  ttukeylem7  10432  alephval2  10490  gchor  10545  fpwwe2lem6  10554  fpwwe2lem11  10559  fpwwe2  10561  pwfseqlem4a  10579  pwfseqlem4  10580  winalim2  10614  gchina  10617  inar1  10693  nqereq  10853  prlem934  10951  prlem936  10965  addsrmo  10991  mulsrmo  10992  supsrlem  11029  axpre-sup  11087  dedekind  11304  dedekindle  11305  mulge0b  12021  supaddc  12118  supmul1  12120  un0addcl  12465  un0mulcl  12466  uzwo3  12888  qbtwnre  13146  xlemul1a  13235  seqcl2  13977  seqfveq2  13981  seqshft2  13985  monoord  13989  seqsplit  13992  seqf1olem1  13998  seqid2  14005  seqhomo  14006  expnegz  14053  expcan  14126  ltexp2  14127  discr  14197  bcval5  14275  hashbc  14410  hashf1lem2  14413  seqcoll  14421  seqcoll2  14422  wrdind  14679  wrd2ind  14680  cau3lem  15312  ello1d  15480  lo1bdd2  15481  rlimclim  15503  climrlim2  15504  rlimdm  15508  rlimcn1  15545  reccn2  15554  rlimsqzlem  15606  lo1le  15609  caucvgrlem  15630  caurcvg2  15635  summolem2  15673  zsum  15675  fsum  15677  fsumf1o  15680  sumss  15681  fsumss  15682  fsumcl2lem  15688  fsumadd  15697  fsumcom2  15731  fsum0diag2  15740  fsummulc2  15741  fsumconst  15747  fsumrelem  15765  fsumrlim  15769  fsumo1  15770  divrcnv  15812  geomulcvg  15836  mertenslem2  15845  prodmolem2  15895  zprod  15897  fprod  15901  fprodf1o  15906  prodss  15907  fprodss  15908  fprodcl2lem  15910  fprodmul  15920  fproddiv  15921  fprodconst  15938  fprodn0  15939  fprodcom2  15944  ruclem8  16199  dvds0lem  16230  dvdsnegb  16237  dvdssub2  16265  bitsf1  16410  bitsshft  16439  bezoutlem3  16505  bezoutlem4  16506  isprm5  16672  isprm6  16679  hashgcdeq  16755  modprminv  16765  modprminveq  16766  reumodprminv  16770  pcqmul  16819  pcqcl  16822  pcxnn0cl  16826  pcxcl  16827  pc2dvds  16845  pcadd  16855  pcmpt  16858  pockthg  16872  infpnlem1  16876  prmreclem5  16886  vdwlem2  16948  vdwlem9  16955  vdwlem10  16956  vdwlem12  16958  ramub  16979  0ram  16986  ramub1lem2  16993  ramub1  16994  ramcl  16995  mreexexd  17609  acsfn2  17624  iscatd  17634  catpropd  17670  setcmon  18049  pleval2i  18295  psss  18541  mgmidsssn0  18635  mgmhmeql  18679  mhmeql  18789  frmdss2  18826  frmdup3  18830  grprcan  18944  dfgrp3lem  19009  mulgnn0ass  19081  isnsg3  19130  ghmpreima  19208  ghmeql  19209  gaorber  19278  f1omvdco2  19418  psgnunilem1  19463  psgnunilem2  19465  oddvds  19517  gexdvds  19554  sylow1lem1  19568  odcau  19574  pgpssslw  19584  sylow2alem2  19588  sylow2blem3  19592  fislw  19595  lsmmod  19645  efgredlem  19717  frgpup3  19748  gsumval3  19877  gsumzres  19879  gsumzcl2  19880  gsumzf1o  19882  gsumzaddlem  19891  gsumconst  19904  gsumzmhm  19907  gsumzoppg  19914  gsum2d2lem  19943  ablfac1eulem  20044  pgpfac1lem5  20051  ablfaclem3  20059  issubdrg  20752  lss1d  20953  lmhmeql  21046  lspextmo  21047  lspsnat  21139  lsppratlem6  21146  islbs3  21149  lbsextlem4  21155  lidl1el  21220  cnsubrg  21421  gsumfsum  21428  prmirredlem  21466  znidomb  21555  frgpcyg  21567  cssmre  21687  dsmmsubg  21737  dsmmlss  21738  frlmsslsp  21790  lindff1  21814  lindfrn  21815  rnasclassa  21889  mvrf1  21978  mplsubglem  21991  mpllsslem  21992  mplcoe1  22029  mplcoe5  22032  gsummoncoe1  22287  mat1dimcrng  22456  mdetdiaglem  22577  mdetunilem7  22597  mdetunilem8  22598  mdetunilem9  22599  cpmatacl  22695  cpmatmcllem  22697  mp2pm2mplem4  22788  en2top  22964  toponmre  23072  topssnei  23103  innei  23104  clslp  23127  restcls  23160  restntr  23161  ordtrest2lem  23182  cnpco  23246  cncls2  23252  cncnpi  23257  cncnp  23259  cnconst2  23262  cnpdis  23272  lmcnp  23283  cnhaus  23333  isreg2  23356  cncmp  23371  tgcmp  23380  sscmp  23384  cmpfi  23387  cnconn  23401  iunconnlem  23406  clsconn  23409  1stcfb  23424  1stcrest  23432  2ndcctbss  23434  2ndcdisj  23435  1stcelcls  23440  1stccnp  23441  restnlly  23461  cldllycmp  23474  lly1stc  23475  dislly  23476  locfincmp  23505  comppfsc  23511  kgentopon  23517  kgenidm  23526  1stckgenlem  23532  kgencn3  23537  ptpjpre1  23550  ptbasin  23556  txcls  23583  tx2cn  23589  ptpjcn  23590  ptclsg  23594  ptcnp  23601  txdis  23611  txlly  23615  txnlly  23616  pthaus  23617  txtube  23619  txcmplem1  23620  txcmplem2  23621  txcmp  23622  txhaus  23626  txkgen  23631  xkohaus  23632  xkococnlem  23638  xkococn  23639  txconn  23668  qtopeu  23695  qtoprest  23696  regr1lem2  23719  kqreglem1  23720  cmphaushmeo  23779  xkocnv  23793  fgabs  23858  filuni  23864  trufil  23889  ufileu  23898  filufint  23899  fin1aufil  23911  elfm2  23927  rnelfmlem  23931  fmfnfmlem2  23934  fmfnfmlem4  23936  fmufil  23938  flimopn  23954  fbflim2  23956  hausflimi  23959  hausflim  23960  flimcf  23961  flimclslem  23963  flimsncls  23965  hauspwpwf1  23966  cnpflfi  23978  fclsnei  23998  fclscf  24004  flimfnfcls  24007  fclscmp  24009  ufilcmp  24011  fcfnei  24014  cnpfcf  24020  alexsublem  24023  alexsub  24024  alexsubALTlem2  24027  alexsubALTlem3  24028  alexsubALTlem4  24029  ptcmplem3  24033  ptcmplem4  24034  ptcmplem5  24035  symgtgp  24085  tgpconncompeqg  24091  tgpconncomp  24092  ghmcnp  24094  tgpt0  24098  qustgplem  24100  haustsms2  24116  tsmsgsum  24118  tsmsres  24123  tsmsxp  24134  imasdsf1olem  24352  xbln0  24393  blssps  24403  blss  24404  neibl  24480  blcld  24484  metss  24487  metequiv2  24489  met1stc  24500  metrest  24503  prdsxmslem2  24508  metcnp3  24519  nrmmetd  24553  nlmvscnlem1  24665  nrginvrcnlem  24670  nmoleub  24710  icccmplem2  24803  icccmp  24805  reconnlem2  24807  xrge0tsms  24814  metdstri  24831  metdseq0  24834  metdscn  24836  cnmpopc  24909  lebnumlem3  24944  pcoval2  24997  pcopt  25003  nmoleub2lem  25095  nmhmcn  25101  ipcnlem1  25226  cfilfcls  25255  cmetcaulem  25269  iscmet3lem2  25273  iscmet3  25274  equivcau  25281  caubl  25289  bcthlem2  25306  bcthlem3  25307  bcthlem4  25308  bcthlem5  25309  ivthlem2  25433  ivthlem3  25434  ovoliunlem2  25484  ovolicc2lem2  25499  ovolicc2lem5  25502  ovolicc2  25503  ismbl2  25508  nulmbl  25516  nulmbl2  25517  unmbl  25518  shftmbl  25519  voliunlem3  25533  volsup  25537  ioombl1lem4  25542  ioombl1  25543  icombl  25545  ioombl  25546  uniioombl  25570  opnmbllem  25582  volivth  25588  vitali  25594  mbflimsup  25647  i1fadd  25676  itg1addlem4  25680  itg2le  25720  itg2seq  25723  itg2lea  25725  itg2splitlem  25729  itg2split  25730  itg2mono  25734  itg2gt0  25741  itg2cnlem2  25743  itgss  25793  itgfsum  25808  itgcn  25826  ellimc3  25860  limcco  25874  limciun  25875  dvnres  25912  dvnfre  25933  rolle  25971  c1liplem1  25977  dvivth  25991  dvne0  25992  lhop1lem  25994  lhop1  25995  lhop  25997  dvcnvrelem1  25998  dvfsumrlim  26012  dvfsum2  26015  ftc1a  26018  ftc1lem6  26022  itgsubst  26030  tdeglem4  26039  mdegaddle  26053  mdegvscale  26054  mdegmullem  26057  deg1tmle  26097  ply1divex  26116  dvdsq1p  26142  fta1g  26149  fta1b  26151  plyco0  26171  coeeulem  26203  dgrlem  26208  plyco  26220  coemullem  26229  dgreq0  26244  dgrco  26254  plydivex  26278  quotcan  26290  aannenlem1  26309  aalioulem2  26314  aalioulem3  26315  taylthlem1  26354  ulmbdd  26380  itgulm  26390  radcnvlt1  26400  psercnlem1  26407  abelthlem2  26414  abelthlem8  26421  logcnlem5  26627  efopn  26639  cxpmul2z  26672  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  27192  perfectlem2  27211  dchrfi  27236  dchrptlem1  27245  dchrptlem2  27246  dchrptlem3  27247  dchrsum2  27249  bposlem1  27265  bposlem3  27267  2sqlem5  27403  2sqlem6  27404  2sqlem8  27407  2sqlem10  27409  2sqb  27413  chebbnd1lem1  27450  chtppilimlem2  27455  dchrisum0flb  27491  dchrisum0fno1  27492  dchrisum0  27501  pntrsumbnd2  27548  pntpbnd1  27567  pntpbnd2  27568  pntlemp  27591  pnt3  27593  qabvle  27606  ostth2lem2  27615  ostth3  27619  ostth  27620  nolt02o  27677  nogt01o  27678  nosupprefixmo  27682  noinfprefixmo  27683  nosupbnd1lem3  27692  nosupbnd1lem4  27693  nosupbnd1lem5  27694  noinfbnd1lem3  27707  noinfbnd1lem4  27708  noinfbnd1lem5  27709  noetasuplem4  27718  noetainflem4  27722  etaslts  27803  cuteq1  27827  madebdaylemlrcut  27909  cutlt  27942  mulsuniflem  28159  bdayons  28286  addonbday  28289  om2noseqlt  28309  n0fincut  28365  bdaypw2n0bndlem  28473  bdayfinbndlem1  28477  z12sge0  28493  readdscl  28509  remulscl  28512  colinearalglem4  28996  axcontlem10  29060  upgrex  29179  smcnlem  30787  ubthlem1  30960  ubthlem3  30962  htthlem  31007  5oalem6  31749  leopmuli  32223  pjnormssi  32258  pjclem4  32289  pj3si  32297  hatomistici  32452  sumdmdlem  32508  sgn3da  32926  wrdt2ind  33032  xrge0tsmsd  33153  isarchiofld  33279  ordtrest2NEWlem  34086  qqhf  34150  eulerpartlemb  34532  ballotlemfc0  34657  ballotlemfcc  34658  subfacp1lem5  35386  erdszelem7  35399  erdszelem11  35403  pconnconn  35433  txpconn  35434  connpconn  35437  sconnpi1  35441  txsconn  35443  cvxsconn  35445  cvmopnlem  35480  cvmfolem  35481  cvmliftmolem2  35484  cvmliftlem7  35493  cvmliftlem10  35496  cvmlift2lem10  35514  cvmlift3lem4  35524  cvmlift3lem8  35528  satfun  35613  msubff1  35758  wzel  36024  wsuclem  36025  btwnouttr2  36224  cgrxfr  36257  btwnxfr  36258  brcolinear  36261  lineext  36278  btwnconn1lem13  36301  midofsegid  36306  segcon2  36307  brsegle  36310  seglecgr12im  36312  segletr  36316  colinbtwnle  36320  broutsideof2  36324  btwnoutside  36327  broutsideof3  36328  outsideoftr  36331  outsideofeq  36332  outsideofeu  36333  outsidele  36334  lineunray  36349  lineelsb2  36350  linethru  36355  finminlem  36520  nn0prpwlem  36524  neibastop2lem  36562  neibastop2  36563  neibastop3  36564  topjoin  36567  tailfb  36579  axtcond  36680  relowlssretop  37697  fvineqsneq  37746  wl-sbcom2d-lem1  37902  finixpnum  37944  poimirlem6  37965  poimirlem7  37966  poimirlem13  37972  poimirlem26  37985  poimirlem29  37988  heicant  37994  opnmbllem0  37995  mblfinlem3  37998  ismblfin  38000  ovoliunnfl  38001  voliunnfl  38003  volsupnfl  38004  itg2addnclem  38010  itg2addnclem3  38012  ftc1cnnc  38031  sdclem2  38081  fdc  38084  istotbnd3  38110  isbnd2  38122  isbnd3  38123  prdsbnd  38132  cntotbnd  38135  heibor1lem  38148  heibor1  38149  heiborlem10  38159  rrncmslem  38171  ghomco  38230  1idl  38365  unichnidl  38370  disjlem18  39242  prtlem10  39329  prtlem18  39341  atlatmstc  39783  cvrexchlem  39883  paddasslem14  40297  pexmidlem5N  40438  cdleme29ex  40838  cdlemefr29exN  40866  cdleme32fva  40901  diarnN  41593  dihlsscpre  41698  isnacs3  43160  fnwe2lem2  43501  kelac1  43513  hbtlem5  43578  hbt  43580  dgraa0p  43599  ofoafg  43804  ofoafo  43806  naddcnffo  43814  fzunt  43904  fzuntd  43905  monoordxrv  45931  rlimdmafv  47641  rlimdmafv2  47722  fmtnoprmfac2  48046  perfectALTVlem2  48214  mogoldbb  48277  lindslinindsimp2  48955