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  3139  reximddv  3153  disjxiun  5096  wereu2  5622  frpomin  6299  ordtr3  6364  fcof1  7235  knatar  7305  riota5f  7345  ovmpodf  7516  extmptsuppeq  8132  suppss  8138  suppss2  8144  frrlem14  8243  fprresex  8254  smoord  8299  tfrlem9a  8319  oaass  8490  oelimcl  8530  oaabs2  8579  cofon1  8602  naddssim  8615  swoso  8672  eceqoveq  8763  domdifsn  8992  domunsncan  9009  omxpenlem  9010  enfixsn  9018  mapdom2  9080  frfi  9189  fofinf1o  9236  finsschain  9263  elfiun  9337  marypha1lem  9340  eqsupd  9364  eqinfd  9393  ordiso2  9424  ordtypelem6  9432  ordtypelem7  9433  ordtypelem10  9436  oismo  9449  wemapsolem  9459  brwdom2  9482  wdomtr  9484  unwdomg  9493  xpwdomg  9494  unxpwdom2  9497  cantnfval2  9582  cantnfle  9584  cantnflem1  9602  cantnf  9606  r1ordg  9694  tcrank  9800  carddomi2  9886  harval2  9913  infxpenlem  9927  infxpenc2lem2  9934  fseqenlem1  9938  dfac8clem  9946  acndom2  9968  infpwfien  9976  iunfictbso  10028  dfac12lem3  10060  infxp  10128  coflim  10175  cofsmo  10183  coftr  10187  sornom  10191  infpssrlem4  10220  enfin2i  10235  fin23lem26  10239  fin23lem27  10242  fin23lem36  10262  fin23lem40  10265  isf32lem5  10271  isf34lem4  10291  isfin1-3  10300  fin1a2lem10  10323  fin1a2lem13  10326  fin1a2s  10328  hsmexlem4  10343  ttukeylem5  10427  ttukeylem6  10428  ttukeylem7  10429  alephval2  10487  gchor  10542  fpwwe2lem6  10551  fpwwe2lem11  10556  fpwwe2  10558  pwfseqlem4a  10576  pwfseqlem4  10577  winalim2  10611  gchina  10614  inar1  10690  nqereq  10850  prlem934  10948  prlem936  10962  addsrmo  10988  mulsrmo  10989  supsrlem  11026  axpre-sup  11084  dedekind  11300  dedekindle  11301  mulge0b  12016  supaddc  12113  supmul1  12115  un0addcl  12438  un0mulcl  12439  uzwo3  12860  qbtwnre  13118  xlemul1a  13207  seqcl2  13947  seqfveq2  13951  seqshft2  13955  monoord  13959  seqsplit  13962  seqf1olem1  13968  seqid2  13975  seqhomo  13976  expnegz  14023  expcan  14096  ltexp2  14097  discr  14167  bcval5  14245  hashbc  14380  hashf1lem2  14383  seqcoll  14391  seqcoll2  14392  wrdind  14649  wrd2ind  14650  cau3lem  15282  ello1d  15450  lo1bdd2  15451  rlimclim  15473  climrlim2  15474  rlimdm  15478  rlimcn1  15515  reccn2  15524  rlimsqzlem  15576  lo1le  15579  caucvgrlem  15600  caurcvg2  15605  summolem2  15643  zsum  15645  fsum  15647  fsumf1o  15650  sumss  15651  fsumss  15652  fsumcl2lem  15658  fsumadd  15667  fsumcom2  15701  fsum0diag2  15710  fsummulc2  15711  fsumconst  15717  fsumrelem  15734  fsumrlim  15738  fsumo1  15739  divrcnv  15779  geomulcvg  15803  mertenslem2  15812  prodmolem2  15862  zprod  15864  fprod  15868  fprodf1o  15873  prodss  15874  fprodss  15875  fprodcl2lem  15877  fprodmul  15887  fproddiv  15888  fprodconst  15905  fprodn0  15906  fprodcom2  15911  ruclem8  16166  dvds0lem  16197  dvdsnegb  16204  dvdssub2  16232  bitsf1  16377  bitsshft  16406  bezoutlem3  16472  bezoutlem4  16473  isprm5  16638  isprm6  16645  hashgcdeq  16721  modprminv  16731  modprminveq  16732  reumodprminv  16736  pcqmul  16785  pcqcl  16788  pcxnn0cl  16792  pcxcl  16793  pc2dvds  16811  pcadd  16821  pcmpt  16824  pockthg  16838  infpnlem1  16842  prmreclem5  16852  vdwlem2  16914  vdwlem9  16921  vdwlem10  16922  vdwlem12  16924  ramub  16945  0ram  16952  ramub1lem2  16959  ramub1  16960  ramcl  16961  mreexexd  17575  acsfn2  17590  iscatd  17600  catpropd  17636  setcmon  18015  pleval2i  18261  psss  18507  mgmidsssn0  18601  mgmhmeql  18645  mhmeql  18755  frmdss2  18792  frmdup3  18796  grprcan  18907  dfgrp3lem  18972  mulgnn0ass  19044  isnsg3  19093  ghmpreima  19171  ghmeql  19172  gaorber  19241  f1omvdco2  19381  psgnunilem1  19426  psgnunilem2  19428  oddvds  19480  gexdvds  19517  sylow1lem1  19531  odcau  19537  pgpssslw  19547  sylow2alem2  19551  sylow2blem3  19555  fislw  19558  lsmmod  19608  efgredlem  19680  frgpup3  19711  gsumval3  19840  gsumzres  19842  gsumzcl2  19843  gsumzf1o  19845  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsumzoppg  19877  gsum2d2lem  19906  ablfac1eulem  20007  pgpfac1lem5  20014  ablfaclem3  20022  issubdrg  20717  lss1d  20918  lmhmeql  21011  lspextmo  21012  lspsnat  21104  lsppratlem6  21111  islbs3  21114  lbsextlem4  21120  lidl1el  21185  cnsubrg  21386  gsumfsum  21393  prmirredlem  21431  znidomb  21520  frgpcyg  21532  cssmre  21652  dsmmsubg  21702  dsmmlss  21703  frlmsslsp  21755  lindff1  21779  lindfrn  21780  rnasclassa  21855  mvrf1  21945  mplsubglem  21958  mpllsslem  21959  mplcoe1  21996  mplcoe5  21999  gsummoncoe1  22256  mat1dimcrng  22425  mdetdiaglem  22546  mdetunilem7  22566  mdetunilem8  22567  mdetunilem9  22568  cpmatacl  22664  cpmatmcllem  22666  mp2pm2mplem4  22757  en2top  22933  toponmre  23041  topssnei  23072  innei  23073  clslp  23096  restcls  23129  restntr  23130  ordtrest2lem  23151  cnpco  23215  cncls2  23221  cncnpi  23226  cncnp  23228  cnconst2  23231  cnpdis  23241  lmcnp  23252  cnhaus  23302  isreg2  23325  cncmp  23340  tgcmp  23349  sscmp  23353  cmpfi  23356  cnconn  23370  iunconnlem  23375  clsconn  23378  1stcfb  23393  1stcrest  23401  2ndcctbss  23403  2ndcdisj  23404  1stcelcls  23409  1stccnp  23410  restnlly  23430  cldllycmp  23443  lly1stc  23444  dislly  23445  locfincmp  23474  comppfsc  23480  kgentopon  23486  kgenidm  23495  1stckgenlem  23501  kgencn3  23506  ptpjpre1  23519  ptbasin  23525  txcls  23552  tx2cn  23558  ptpjcn  23559  ptclsg  23563  ptcnp  23570  txdis  23580  txlly  23584  txnlly  23585  pthaus  23586  txtube  23588  txcmplem1  23589  txcmplem2  23590  txcmp  23591  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  xkococn  23608  txconn  23637  qtopeu  23664  qtoprest  23665  regr1lem2  23688  kqreglem1  23689  cmphaushmeo  23748  xkocnv  23762  fgabs  23827  filuni  23833  trufil  23858  ufileu  23867  filufint  23868  fin1aufil  23880  elfm2  23896  rnelfmlem  23900  fmfnfmlem2  23903  fmfnfmlem4  23905  fmufil  23907  flimopn  23923  fbflim2  23925  hausflimi  23928  hausflim  23929  flimcf  23930  flimclslem  23932  flimsncls  23934  hauspwpwf1  23935  cnpflfi  23947  fclsnei  23967  fclscf  23973  flimfnfcls  23976  fclscmp  23978  ufilcmp  23980  fcfnei  23983  cnpfcf  23989  alexsublem  23992  alexsub  23993  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem3  24002  ptcmplem4  24003  ptcmplem5  24004  symgtgp  24054  tgpconncompeqg  24060  tgpconncomp  24061  ghmcnp  24063  tgpt0  24067  qustgplem  24069  haustsms2  24085  tsmsgsum  24087  tsmsres  24092  tsmsxp  24103  imasdsf1olem  24321  xbln0  24362  blssps  24372  blss  24373  neibl  24449  blcld  24453  metss  24456  metequiv2  24458  met1stc  24469  metrest  24472  prdsxmslem2  24477  metcnp3  24488  nrmmetd  24522  nlmvscnlem1  24634  nrginvrcnlem  24639  nmoleub  24679  icccmplem2  24772  icccmp  24774  reconnlem2  24776  xrge0tsms  24783  metdstri  24800  metdseq0  24803  metdscn  24805  cnmpopc  24882  lebnumlem3  24922  pcoval2  24976  pcopt  24982  nmoleub2lem  25074  nmhmcn  25080  ipcnlem1  25205  cfilfcls  25234  cmetcaulem  25248  iscmet3lem2  25252  iscmet3  25253  equivcau  25260  caubl  25268  bcthlem2  25285  bcthlem3  25286  bcthlem4  25287  bcthlem5  25288  ivthlem2  25413  ivthlem3  25414  ovoliunlem2  25464  ovolicc2lem2  25479  ovolicc2lem5  25482  ovolicc2  25483  ismbl2  25488  nulmbl  25496  nulmbl2  25497  unmbl  25498  shftmbl  25499  voliunlem3  25513  volsup  25517  ioombl1lem4  25522  ioombl1  25523  icombl  25525  ioombl  25526  uniioombl  25550  opnmbllem  25562  volivth  25568  vitali  25574  mbflimsup  25627  i1fadd  25656  itg1addlem4  25660  itg2le  25700  itg2seq  25703  itg2lea  25705  itg2splitlem  25709  itg2split  25710  itg2mono  25714  itg2gt0  25721  itg2cnlem2  25723  itgss  25773  itgfsum  25788  itgcn  25806  ellimc3  25840  limcco  25854  limciun  25855  dvnres  25893  dvnfre  25916  rolle  25954  c1liplem1  25961  dvivth  25975  dvne0  25976  lhop1lem  25978  lhop1  25979  lhop  25981  dvcnvrelem1  25982  dvfsumrlim  25998  dvfsum2  26001  ftc1a  26004  ftc1lem6  26008  itgsubst  26016  tdeglem4  26025  mdegaddle  26039  mdegvscale  26040  mdegmullem  26043  deg1tmle  26083  ply1divex  26102  dvdsq1p  26128  fta1g  26135  fta1b  26137  plyco0  26157  coeeulem  26189  dgrlem  26194  plyco  26206  coemullem  26215  dgreq0  26231  dgrco  26241  plydivex  26265  quotcan  26277  aannenlem1  26296  aalioulem2  26301  aalioulem3  26302  taylthlem1  26341  ulmbdd  26367  itgulm  26377  radcnvlt1  26387  psercnlem1  26395  abelthlem2  26402  abelthlem8  26409  logcnlem5  26615  efopn  26627  cxpmul2z  26660  cxpcn3lem  26717  cxpeq  26727  xrlimcnp  26938  cxplim  26942  o1cxp  26945  cxploglim  26948  scvxcvx  26956  jensen  26959  ftalem1  27043  ftalem2  27044  fta  27050  basellem3  27053  isppw2  27085  ppinprm  27122  chtnprm  27124  mpodvdsmulf1o  27164  dvdsmulf1o  27166  chtublem  27182  perfectlem2  27201  dchrfi  27226  dchrptlem1  27235  dchrptlem2  27236  dchrptlem3  27237  dchrsum2  27239  bposlem1  27255  bposlem3  27257  2sqlem5  27393  2sqlem6  27394  2sqlem8  27397  2sqlem10  27399  2sqb  27403  chebbnd1lem1  27440  chtppilimlem2  27445  dchrisum0flb  27481  dchrisum0fno1  27482  dchrisum0  27491  pntrsumbnd2  27538  pntpbnd1  27557  pntpbnd2  27558  pntlemp  27581  pnt3  27583  qabvle  27596  ostth2lem2  27605  ostth3  27609  ostth  27610  nolt02o  27667  nogt01o  27668  nosupprefixmo  27672  noinfprefixmo  27673  nosupbnd1lem3  27682  nosupbnd1lem4  27683  nosupbnd1lem5  27684  noinfbnd1lem3  27697  noinfbnd1lem4  27698  noinfbnd1lem5  27699  noetasuplem4  27708  noetainflem4  27712  etasslt  27791  cuteq1  27815  madebdaylemlrcut  27881  cutlt  27914  mulsuniflem  28131  bdayon  28257  addsonbday  28260  om2noseqlt  28280  n0sfincut  28335  bdaypw2n0sbndlem  28442  bdayfinbndlem1  28446  zs12ge0  28462  readdscl  28478  remulscl  28481  colinearalglem4  28965  axcontlem10  29029  upgrex  29148  smcnlem  30755  ubthlem1  30928  ubthlem3  30930  htthlem  30975  5oalem6  31717  leopmuli  32191  pjnormssi  32226  pjclem4  32257  pj3si  32265  hatomistici  32420  sumdmdlem  32476  sgn3da  32896  wrdt2ind  33016  xrge0tsmsd  33136  isarchiofld  33262  ordtrest2NEWlem  34060  qqhf  34124  eulerpartlemb  34506  ballotlemfc0  34631  ballotlemfcc  34632  subfacp1lem5  35359  erdszelem7  35372  erdszelem11  35376  pconnconn  35406  txpconn  35407  connpconn  35410  sconnpi1  35414  txsconn  35416  cvxsconn  35418  cvmopnlem  35453  cvmfolem  35454  cvmliftmolem2  35457  cvmliftlem7  35466  cvmliftlem10  35469  cvmlift2lem10  35487  cvmlift3lem4  35497  cvmlift3lem8  35501  satfun  35586  msubff1  35731  wzel  35997  wsuclem  35998  btwnouttr2  36197  cgrxfr  36230  btwnxfr  36231  brcolinear  36234  lineext  36251  btwnconn1lem13  36274  midofsegid  36279  segcon2  36280  brsegle  36283  seglecgr12im  36285  segletr  36289  colinbtwnle  36293  broutsideof2  36297  btwnoutside  36300  broutsideof3  36301  outsideoftr  36304  outsideofeq  36305  outsideofeu  36306  outsidele  36307  lineunray  36322  lineelsb2  36323  linethru  36328  finminlem  36493  nn0prpwlem  36497  neibastop2lem  36535  neibastop2  36536  neibastop3  36537  topjoin  36540  tailfb  36552  relowlssretop  37539  fvineqsneq  37588  wl-sbcom2d-lem1  37735  finixpnum  37777  poimirlem6  37798  poimirlem7  37799  poimirlem13  37805  poimirlem26  37818  poimirlem29  37821  heicant  37827  opnmbllem0  37828  mblfinlem3  37831  ismblfin  37833  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  itg2addnclem  37843  itg2addnclem3  37845  ftc1cnnc  37864  sdclem2  37914  fdc  37917  istotbnd3  37943  isbnd2  37955  isbnd3  37956  prdsbnd  37965  cntotbnd  37968  heibor1lem  37981  heibor1  37982  heiborlem10  37992  rrncmslem  38004  ghomco  38063  1idl  38198  unichnidl  38203  disjlem18  39075  prtlem10  39162  prtlem18  39174  atlatmstc  39616  cvrexchlem  39716  paddasslem14  40130  pexmidlem5N  40271  cdleme29ex  40671  cdlemefr29exN  40699  cdleme32fva  40734  diarnN  41426  dihlsscpre  41531  isnacs3  42988  fnwe2lem2  43329  kelac1  43341  hbtlem5  43406  hbt  43408  dgraa0p  43427  ofoafg  43632  ofoafo  43634  naddcnffo  43642  fzunt  43732  fzuntd  43733  monoordxrv  45761  rlimdmafv  47459  rlimdmafv2  47540  fmtnoprmfac2  47849  perfectALTVlem2  48004  mogoldbb  48067  lindslinindsimp2  48745