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  5082  wereu2  5628  frpomin  6304  ordtr3  6369  fcof1  7242  knatar  7312  riota5f  7352  ovmpodf  7523  extmptsuppeq  8138  suppss  8144  suppss2  8150  frrlem14  8249  fprresex  8260  smoord  8305  tfrlem9a  8325  oaass  8496  oelimcl  8536  oaabs2  8585  cofon1  8608  naddssim  8621  swoso  8678  eceqoveq  8769  domdifsn  8998  domunsncan  9015  omxpenlem  9016  enfixsn  9024  mapdom2  9086  frfi  9195  fofinf1o  9242  finsschain  9269  elfiun  9343  marypha1lem  9346  eqsupd  9370  eqinfd  9399  ordiso2  9430  ordtypelem6  9438  ordtypelem7  9439  ordtypelem10  9442  oismo  9455  wemapsolem  9465  brwdom2  9488  wdomtr  9490  unwdomg  9499  xpwdomg  9500  unxpwdom2  9503  cantnfval2  9590  cantnfle  9592  cantnflem1  9610  cantnf  9614  r1ordg  9702  tcrank  9808  carddomi2  9894  harval2  9921  infxpenlem  9935  infxpenc2lem2  9942  fseqenlem1  9946  dfac8clem  9954  acndom2  9976  infpwfien  9984  iunfictbso  10036  dfac12lem3  10068  infxp  10136  coflim  10183  cofsmo  10191  coftr  10195  sornom  10199  infpssrlem4  10228  enfin2i  10243  fin23lem26  10247  fin23lem27  10250  fin23lem36  10270  fin23lem40  10273  isf32lem5  10279  isf34lem4  10299  isfin1-3  10308  fin1a2lem10  10331  fin1a2lem13  10334  fin1a2s  10336  hsmexlem4  10351  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  alephval2  10495  gchor  10550  fpwwe2lem6  10559  fpwwe2lem11  10564  fpwwe2  10566  pwfseqlem4a  10584  pwfseqlem4  10585  winalim2  10619  gchina  10622  inar1  10698  nqereq  10858  prlem934  10956  prlem936  10970  addsrmo  10996  mulsrmo  10997  supsrlem  11034  axpre-sup  11092  dedekind  11309  dedekindle  11310  mulge0b  12026  supaddc  12123  supmul1  12125  un0addcl  12470  un0mulcl  12471  uzwo3  12893  qbtwnre  13151  xlemul1a  13240  seqcl2  13982  seqfveq2  13986  seqshft2  13990  monoord  13994  seqsplit  13997  seqf1olem1  14003  seqid2  14010  seqhomo  14011  expnegz  14058  expcan  14131  ltexp2  14132  discr  14202  bcval5  14280  hashbc  14415  hashf1lem2  14418  seqcoll  14426  seqcoll2  14427  wrdind  14684  wrd2ind  14685  cau3lem  15317  ello1d  15485  lo1bdd2  15486  rlimclim  15508  climrlim2  15509  rlimdm  15513  rlimcn1  15550  reccn2  15559  rlimsqzlem  15611  lo1le  15614  caucvgrlem  15635  caurcvg2  15640  summolem2  15678  zsum  15680  fsum  15682  fsumf1o  15685  sumss  15686  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  fsumcom2  15736  fsum0diag2  15745  fsummulc2  15746  fsumconst  15752  fsumrelem  15770  fsumrlim  15774  fsumo1  15775  divrcnv  15817  geomulcvg  15841  mertenslem2  15850  prodmolem2  15900  zprod  15902  fprod  15906  fprodf1o  15911  prodss  15912  fprodss  15913  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodconst  15943  fprodn0  15944  fprodcom2  15949  ruclem8  16204  dvds0lem  16235  dvdsnegb  16242  dvdssub2  16270  bitsf1  16415  bitsshft  16444  bezoutlem3  16510  bezoutlem4  16511  isprm5  16677  isprm6  16684  hashgcdeq  16760  modprminv  16770  modprminveq  16771  reumodprminv  16775  pcqmul  16824  pcqcl  16827  pcxnn0cl  16831  pcxcl  16832  pc2dvds  16850  pcadd  16860  pcmpt  16863  pockthg  16877  infpnlem1  16881  prmreclem5  16891  vdwlem2  16953  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  ramub  16984  0ram  16991  ramub1lem2  16998  ramub1  16999  ramcl  17000  mreexexd  17614  acsfn2  17629  iscatd  17639  catpropd  17675  setcmon  18054  pleval2i  18300  psss  18546  mgmidsssn0  18640  mgmhmeql  18684  mhmeql  18794  frmdss2  18831  frmdup3  18835  grprcan  18949  dfgrp3lem  19014  mulgnn0ass  19086  isnsg3  19135  ghmpreima  19213  ghmeql  19214  gaorber  19283  f1omvdco2  19423  psgnunilem1  19468  psgnunilem2  19470  oddvds  19522  gexdvds  19559  sylow1lem1  19573  odcau  19579  pgpssslw  19589  sylow2alem2  19593  sylow2blem3  19597  fislw  19600  lsmmod  19650  efgredlem  19722  frgpup3  19753  gsumval3  19882  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  gsum2d2lem  19948  ablfac1eulem  20049  pgpfac1lem5  20056  ablfaclem3  20064  issubdrg  20757  lss1d  20958  lmhmeql  21050  lspextmo  21051  lspsnat  21143  lsppratlem6  21150  islbs3  21153  lbsextlem4  21159  lidl1el  21224  cnsubrg  21407  gsumfsum  21414  prmirredlem  21452  znidomb  21541  frgpcyg  21553  cssmre  21673  dsmmsubg  21723  dsmmlss  21724  frlmsslsp  21776  lindff1  21800  lindfrn  21801  rnasclassa  21875  mvrf1  21964  mplsubglem  21977  mpllsslem  21978  mplcoe1  22015  mplcoe5  22018  gsummoncoe1  22273  mat1dimcrng  22442  mdetdiaglem  22563  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  cpmatacl  22681  cpmatmcllem  22683  mp2pm2mplem4  22774  en2top  22950  toponmre  23058  topssnei  23089  innei  23090  clslp  23113  restcls  23146  restntr  23147  ordtrest2lem  23168  cnpco  23232  cncls2  23238  cncnpi  23243  cncnp  23245  cnconst2  23248  cnpdis  23258  lmcnp  23269  cnhaus  23319  isreg2  23342  cncmp  23357  tgcmp  23366  sscmp  23370  cmpfi  23373  cnconn  23387  iunconnlem  23392  clsconn  23395  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  2ndcdisj  23421  1stcelcls  23426  1stccnp  23427  restnlly  23447  cldllycmp  23460  lly1stc  23461  dislly  23462  locfincmp  23491  comppfsc  23497  kgentopon  23503  kgenidm  23512  1stckgenlem  23518  kgencn3  23523  ptpjpre1  23536  ptbasin  23542  txcls  23569  tx2cn  23575  ptpjcn  23576  ptclsg  23580  ptcnp  23587  txdis  23597  txlly  23601  txnlly  23602  pthaus  23603  txtube  23605  txcmplem1  23606  txcmplem2  23607  txcmp  23608  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  xkococn  23625  txconn  23654  qtopeu  23681  qtoprest  23682  regr1lem2  23705  kqreglem1  23706  cmphaushmeo  23765  xkocnv  23779  fgabs  23844  filuni  23850  trufil  23875  ufileu  23884  filufint  23885  fin1aufil  23897  elfm2  23913  rnelfmlem  23917  fmfnfmlem2  23920  fmfnfmlem4  23922  fmufil  23924  flimopn  23940  fbflim2  23942  hausflimi  23945  hausflim  23946  flimcf  23947  flimclslem  23949  flimsncls  23951  hauspwpwf1  23952  cnpflfi  23964  fclsnei  23984  fclscf  23990  flimfnfcls  23993  fclscmp  23995  ufilcmp  23997  fcfnei  24000  cnpfcf  24006  alexsublem  24009  alexsub  24010  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem3  24019  ptcmplem4  24020  ptcmplem5  24021  symgtgp  24071  tgpconncompeqg  24077  tgpconncomp  24078  ghmcnp  24080  tgpt0  24084  qustgplem  24086  haustsms2  24102  tsmsgsum  24104  tsmsres  24109  tsmsxp  24120  imasdsf1olem  24338  xbln0  24379  blssps  24389  blss  24390  neibl  24466  blcld  24470  metss  24473  metequiv2  24475  met1stc  24486  metrest  24489  prdsxmslem2  24494  metcnp3  24505  nrmmetd  24539  nlmvscnlem1  24651  nrginvrcnlem  24656  nmoleub  24696  icccmplem2  24789  icccmp  24791  reconnlem2  24793  xrge0tsms  24800  metdstri  24817  metdseq0  24820  metdscn  24822  cnmpopc  24895  lebnumlem3  24930  pcoval2  24983  pcopt  24989  nmoleub2lem  25081  nmhmcn  25087  ipcnlem1  25212  cfilfcls  25241  cmetcaulem  25255  iscmet3lem2  25259  iscmet3  25260  equivcau  25267  caubl  25275  bcthlem2  25292  bcthlem3  25293  bcthlem4  25294  bcthlem5  25295  ivthlem2  25419  ivthlem3  25420  ovoliunlem2  25470  ovolicc2lem2  25485  ovolicc2lem5  25488  ovolicc2  25489  ismbl2  25494  nulmbl  25502  nulmbl2  25503  unmbl  25504  shftmbl  25505  voliunlem3  25519  volsup  25523  ioombl1lem4  25528  ioombl1  25529  icombl  25531  ioombl  25532  uniioombl  25556  opnmbllem  25568  volivth  25574  vitali  25580  mbflimsup  25633  i1fadd  25662  itg1addlem4  25666  itg2le  25706  itg2seq  25709  itg2lea  25711  itg2splitlem  25715  itg2split  25716  itg2mono  25720  itg2gt0  25727  itg2cnlem2  25729  itgss  25779  itgfsum  25794  itgcn  25812  ellimc3  25846  limcco  25860  limciun  25861  dvnres  25898  dvnfre  25919  rolle  25957  c1liplem1  25963  dvivth  25977  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop  25983  dvcnvrelem1  25984  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  26230  dgrco  26240  plydivex  26263  quotcan  26275  aannenlem1  26294  aalioulem2  26299  aalioulem3  26300  taylthlem1  26338  ulmbdd  26363  itgulm  26373  radcnvlt1  26383  psercnlem1  26390  abelthlem2  26397  abelthlem8  26404  logcnlem5  26610  efopn  26622  cxpmul2z  26655  cxpcn3lem  26711  cxpeq  26721  xrlimcnp  26932  cxplim  26935  o1cxp  26938  cxploglim  26941  scvxcvx  26949  jensen  26952  ftalem1  27036  ftalem2  27037  fta  27043  basellem3  27046  isppw2  27078  ppinprm  27115  chtnprm  27117  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chtublem  27174  perfectlem2  27193  dchrfi  27218  dchrptlem1  27227  dchrptlem2  27228  dchrptlem3  27229  dchrsum2  27231  bposlem1  27247  bposlem3  27249  2sqlem5  27385  2sqlem6  27386  2sqlem8  27389  2sqlem10  27391  2sqb  27395  chebbnd1lem1  27432  chtppilimlem2  27437  dchrisum0flb  27473  dchrisum0fno1  27474  dchrisum0  27483  pntrsumbnd2  27530  pntpbnd1  27549  pntpbnd2  27550  pntlemp  27573  pnt3  27575  qabvle  27588  ostth2lem2  27597  ostth3  27601  ostth  27602  nolt02o  27659  nogt01o  27660  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  etaslts  27785  cuteq1  27809  madebdaylemlrcut  27891  cutlt  27924  mulsuniflem  28141  bdayons  28268  addonbday  28271  om2noseqlt  28291  n0fincut  28347  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  z12sge0  28475  readdscl  28491  remulscl  28494  colinearalglem4  28978  axcontlem10  29042  upgrex  29161  smcnlem  30768  ubthlem1  30941  ubthlem3  30943  htthlem  30988  5oalem6  31730  leopmuli  32204  pjnormssi  32239  pjclem4  32270  pj3si  32278  hatomistici  32433  sumdmdlem  32489  sgn3da  32907  wrdt2ind  33013  xrge0tsmsd  33134  isarchiofld  33260  ordtrest2NEWlem  34066  qqhf  34130  eulerpartlemb  34512  ballotlemfc0  34637  ballotlemfcc  34638  subfacp1lem5  35366  erdszelem7  35379  erdszelem11  35383  pconnconn  35413  txpconn  35414  connpconn  35417  sconnpi1  35421  txsconn  35423  cvxsconn  35425  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem2  35464  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift2lem10  35494  cvmlift3lem4  35504  cvmlift3lem8  35508  satfun  35593  msubff1  35738  wzel  36004  wsuclem  36005  btwnouttr2  36204  cgrxfr  36237  btwnxfr  36238  brcolinear  36241  lineext  36258  btwnconn1lem13  36281  midofsegid  36286  segcon2  36287  brsegle  36290  seglecgr12im  36292  segletr  36296  colinbtwnle  36300  broutsideof2  36304  btwnoutside  36307  broutsideof3  36308  outsideoftr  36311  outsideofeq  36312  outsideofeu  36313  outsidele  36314  lineunray  36329  lineelsb2  36330  linethru  36335  finminlem  36500  nn0prpwlem  36504  neibastop2lem  36542  neibastop2  36543  neibastop3  36544  topjoin  36547  tailfb  36559  axtcond  36660  relowlssretop  37679  fvineqsneq  37728  wl-sbcom2d-lem1  37884  finixpnum  37926  poimirlem6  37947  poimirlem7  37948  poimirlem13  37954  poimirlem26  37967  poimirlem29  37970  heicant  37976  opnmbllem0  37977  mblfinlem3  37980  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  itg2addnclem3  37994  ftc1cnnc  38013  sdclem2  38063  fdc  38066  istotbnd3  38092  isbnd2  38104  isbnd3  38105  prdsbnd  38114  cntotbnd  38117  heibor1lem  38130  heibor1  38131  heiborlem10  38141  rrncmslem  38153  ghomco  38212  1idl  38347  unichnidl  38352  disjlem18  39224  prtlem10  39311  prtlem18  39323  atlatmstc  39765  cvrexchlem  39865  paddasslem14  40279  pexmidlem5N  40420  cdleme29ex  40820  cdlemefr29exN  40848  cdleme32fva  40883  diarnN  41575  dihlsscpre  41680  isnacs3  43142  fnwe2lem2  43479  kelac1  43491  hbtlem5  43556  hbt  43558  dgraa0p  43577  ofoafg  43782  ofoafo  43784  naddcnffo  43792  fzunt  43882  fzuntd  43883  monoordxrv  45909  rlimdmafv  47625  rlimdmafv2  47706  fmtnoprmfac2  48030  perfectALTVlem2  48198  mogoldbb  48261  lindslinindsimp2  48939