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  846  3expia  1121  rexlimdvaa  3138  reximddv  3152  disjxiun  5095  wereu2  5621  frpomin  6298  ordtr3  6363  fcof1  7233  knatar  7303  riota5f  7343  ovmpodf  7514  extmptsuppeq  8130  suppss  8136  suppss2  8142  frrlem14  8241  fprresex  8252  smoord  8297  tfrlem9a  8317  oaass  8488  oelimcl  8528  oaabs2  8577  cofon1  8600  naddssim  8613  swoso  8670  eceqoveq  8761  domdifsn  8990  domunsncan  9007  omxpenlem  9008  enfixsn  9016  mapdom2  9078  frfi  9187  fofinf1o  9234  finsschain  9261  elfiun  9335  marypha1lem  9338  eqsupd  9362  eqinfd  9391  ordiso2  9422  ordtypelem6  9430  ordtypelem7  9431  ordtypelem10  9434  oismo  9447  wemapsolem  9457  brwdom2  9480  wdomtr  9482  unwdomg  9491  xpwdomg  9492  unxpwdom2  9495  cantnfval2  9580  cantnfle  9582  cantnflem1  9600  cantnf  9604  r1ordg  9692  tcrank  9798  carddomi2  9884  harval2  9911  infxpenlem  9925  infxpenc2lem2  9932  fseqenlem1  9936  dfac8clem  9944  acndom2  9966  infpwfien  9974  iunfictbso  10026  dfac12lem3  10058  infxp  10126  coflim  10173  cofsmo  10181  coftr  10185  sornom  10189  infpssrlem4  10218  enfin2i  10233  fin23lem26  10237  fin23lem27  10240  fin23lem36  10260  fin23lem40  10263  isf32lem5  10269  isf34lem4  10289  isfin1-3  10298  fin1a2lem10  10321  fin1a2lem13  10324  fin1a2s  10326  hsmexlem4  10341  ttukeylem5  10425  ttukeylem6  10426  ttukeylem7  10427  alephval2  10485  gchor  10540  fpwwe2lem6  10549  fpwwe2lem11  10554  fpwwe2  10556  pwfseqlem4a  10574  pwfseqlem4  10575  winalim2  10609  gchina  10612  inar1  10688  nqereq  10848  prlem934  10946  prlem936  10960  addsrmo  10986  mulsrmo  10987  supsrlem  11024  axpre-sup  11082  dedekind  11298  dedekindle  11299  mulge0b  12014  supaddc  12111  supmul1  12113  un0addcl  12436  un0mulcl  12437  uzwo3  12858  qbtwnre  13116  xlemul1a  13205  seqcl2  13945  seqfveq2  13949  seqshft2  13953  monoord  13957  seqsplit  13960  seqf1olem1  13966  seqid2  13973  seqhomo  13974  expnegz  14021  expcan  14094  ltexp2  14095  discr  14165  bcval5  14243  hashbc  14378  hashf1lem2  14381  seqcoll  14389  seqcoll2  14390  wrdind  14647  wrd2ind  14648  cau3lem  15280  ello1d  15448  lo1bdd2  15449  rlimclim  15471  climrlim2  15472  rlimdm  15476  rlimcn1  15513  reccn2  15522  rlimsqzlem  15574  lo1le  15577  caucvgrlem  15598  caurcvg2  15603  summolem2  15641  zsum  15643  fsum  15645  fsumf1o  15648  sumss  15649  fsumss  15650  fsumcl2lem  15656  fsumadd  15665  fsumcom2  15699  fsum0diag2  15708  fsummulc2  15709  fsumconst  15715  fsumrelem  15732  fsumrlim  15736  fsumo1  15737  divrcnv  15777  geomulcvg  15801  mertenslem2  15810  prodmolem2  15860  zprod  15862  fprod  15866  fprodf1o  15871  prodss  15872  fprodss  15873  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodconst  15903  fprodn0  15904  fprodcom2  15909  ruclem8  16164  dvds0lem  16195  dvdsnegb  16202  dvdssub2  16230  bitsf1  16375  bitsshft  16404  bezoutlem3  16470  bezoutlem4  16471  isprm5  16636  isprm6  16643  hashgcdeq  16719  modprminv  16729  modprminveq  16730  reumodprminv  16734  pcqmul  16783  pcqcl  16786  pcxnn0cl  16790  pcxcl  16791  pc2dvds  16809  pcadd  16819  pcmpt  16822  pockthg  16836  infpnlem1  16840  prmreclem5  16850  vdwlem2  16912  vdwlem9  16919  vdwlem10  16920  vdwlem12  16922  ramub  16943  0ram  16950  ramub1lem2  16957  ramub1  16958  ramcl  16959  mreexexd  17573  acsfn2  17588  iscatd  17598  catpropd  17634  setcmon  18013  pleval2i  18259  psss  18505  mgmidsssn0  18599  mgmhmeql  18643  mhmeql  18753  frmdss2  18790  frmdup3  18794  grprcan  18905  dfgrp3lem  18970  mulgnn0ass  19042  isnsg3  19091  ghmpreima  19169  ghmeql  19170  gaorber  19239  f1omvdco2  19379  psgnunilem1  19424  psgnunilem2  19426  oddvds  19478  gexdvds  19515  sylow1lem1  19529  odcau  19535  pgpssslw  19545  sylow2alem2  19549  sylow2blem3  19553  fislw  19556  lsmmod  19606  efgredlem  19678  frgpup3  19709  gsumval3  19838  gsumzres  19840  gsumzcl2  19841  gsumzf1o  19843  gsumzaddlem  19852  gsumconst  19865  gsumzmhm  19868  gsumzoppg  19875  gsum2d2lem  19904  ablfac1eulem  20005  pgpfac1lem5  20012  ablfaclem3  20020  issubdrg  20715  lss1d  20916  lmhmeql  21009  lspextmo  21010  lspsnat  21102  lsppratlem6  21109  islbs3  21112  lbsextlem4  21118  lidl1el  21183  cnsubrg  21384  gsumfsum  21391  prmirredlem  21429  znidomb  21518  frgpcyg  21530  cssmre  21650  dsmmsubg  21700  dsmmlss  21701  frlmsslsp  21753  lindff1  21777  lindfrn  21778  rnasclassa  21853  mvrf1  21943  mplsubglem  21956  mpllsslem  21957  mplcoe1  21994  mplcoe5  21997  gsummoncoe1  22254  mat1dimcrng  22423  mdetdiaglem  22544  mdetunilem7  22564  mdetunilem8  22565  mdetunilem9  22566  cpmatacl  22662  cpmatmcllem  22664  mp2pm2mplem4  22755  en2top  22931  toponmre  23039  topssnei  23070  innei  23071  clslp  23094  restcls  23127  restntr  23128  ordtrest2lem  23149  cnpco  23213  cncls2  23219  cncnpi  23224  cncnp  23226  cnconst2  23229  cnpdis  23239  lmcnp  23250  cnhaus  23300  isreg2  23323  cncmp  23338  tgcmp  23347  sscmp  23351  cmpfi  23354  cnconn  23368  iunconnlem  23373  clsconn  23376  1stcfb  23391  1stcrest  23399  2ndcctbss  23401  2ndcdisj  23402  1stcelcls  23407  1stccnp  23408  restnlly  23428  cldllycmp  23441  lly1stc  23442  dislly  23443  locfincmp  23472  comppfsc  23478  kgentopon  23484  kgenidm  23493  1stckgenlem  23499  kgencn3  23504  ptpjpre1  23517  ptbasin  23523  txcls  23550  tx2cn  23556  ptpjcn  23557  ptclsg  23561  ptcnp  23568  txdis  23578  txlly  23582  txnlly  23583  pthaus  23584  txtube  23586  txcmplem1  23587  txcmplem2  23588  txcmp  23589  txhaus  23593  txkgen  23598  xkohaus  23599  xkococnlem  23605  xkococn  23606  txconn  23635  qtopeu  23662  qtoprest  23663  regr1lem2  23686  kqreglem1  23687  cmphaushmeo  23746  xkocnv  23760  fgabs  23825  filuni  23831  trufil  23856  ufileu  23865  filufint  23866  fin1aufil  23878  elfm2  23894  rnelfmlem  23898  fmfnfmlem2  23901  fmfnfmlem4  23903  fmufil  23905  flimopn  23921  fbflim2  23923  hausflimi  23926  hausflim  23927  flimcf  23928  flimclslem  23930  flimsncls  23932  hauspwpwf1  23933  cnpflfi  23945  fclsnei  23965  fclscf  23971  flimfnfcls  23974  fclscmp  23976  ufilcmp  23978  fcfnei  23981  cnpfcf  23987  alexsublem  23990  alexsub  23991  alexsubALTlem2  23994  alexsubALTlem3  23995  alexsubALTlem4  23996  ptcmplem3  24000  ptcmplem4  24001  ptcmplem5  24002  symgtgp  24052  tgpconncompeqg  24058  tgpconncomp  24059  ghmcnp  24061  tgpt0  24065  qustgplem  24067  haustsms2  24083  tsmsgsum  24085  tsmsres  24090  tsmsxp  24101  imasdsf1olem  24319  xbln0  24360  blssps  24370  blss  24371  neibl  24447  blcld  24451  metss  24454  metequiv2  24456  met1stc  24467  metrest  24470  prdsxmslem2  24475  metcnp3  24486  nrmmetd  24520  nlmvscnlem1  24632  nrginvrcnlem  24637  nmoleub  24677  icccmplem2  24770  icccmp  24772  reconnlem2  24774  xrge0tsms  24781  metdstri  24798  metdseq0  24801  metdscn  24803  cnmpopc  24880  lebnumlem3  24920  pcoval2  24974  pcopt  24980  nmoleub2lem  25072  nmhmcn  25078  ipcnlem1  25203  cfilfcls  25232  cmetcaulem  25246  iscmet3lem2  25250  iscmet3  25251  equivcau  25258  caubl  25266  bcthlem2  25283  bcthlem3  25284  bcthlem4  25285  bcthlem5  25286  ivthlem2  25411  ivthlem3  25412  ovoliunlem2  25462  ovolicc2lem2  25477  ovolicc2lem5  25480  ovolicc2  25481  ismbl2  25486  nulmbl  25494  nulmbl2  25495  unmbl  25496  shftmbl  25497  voliunlem3  25511  volsup  25515  ioombl1lem4  25520  ioombl1  25521  icombl  25523  ioombl  25524  uniioombl  25548  opnmbllem  25560  volivth  25566  vitali  25572  mbflimsup  25625  i1fadd  25654  itg1addlem4  25658  itg2le  25698  itg2seq  25701  itg2lea  25703  itg2splitlem  25707  itg2split  25708  itg2mono  25712  itg2gt0  25719  itg2cnlem2  25721  itgss  25771  itgfsum  25786  itgcn  25804  ellimc3  25838  limcco  25852  limciun  25853  dvnres  25891  dvnfre  25914  rolle  25952  c1liplem1  25959  dvivth  25973  dvne0  25974  lhop1lem  25976  lhop1  25977  lhop  25979  dvcnvrelem1  25980  dvfsumrlim  25996  dvfsum2  25999  ftc1a  26002  ftc1lem6  26006  itgsubst  26014  tdeglem4  26023  mdegaddle  26037  mdegvscale  26038  mdegmullem  26041  deg1tmle  26081  ply1divex  26100  dvdsq1p  26126  fta1g  26133  fta1b  26135  plyco0  26155  coeeulem  26187  dgrlem  26192  plyco  26204  coemullem  26213  dgreq0  26229  dgrco  26239  plydivex  26263  quotcan  26275  aannenlem1  26294  aalioulem2  26299  aalioulem3  26300  taylthlem1  26339  ulmbdd  26365  itgulm  26375  radcnvlt1  26385  psercnlem1  26393  abelthlem2  26400  abelthlem8  26407  logcnlem5  26613  efopn  26625  cxpmul2z  26658  cxpcn3lem  26715  cxpeq  26725  xrlimcnp  26936  cxplim  26940  o1cxp  26943  cxploglim  26946  scvxcvx  26954  jensen  26957  ftalem1  27041  ftalem2  27042  fta  27048  basellem3  27051  isppw2  27083  ppinprm  27120  chtnprm  27122  mpodvdsmulf1o  27162  dvdsmulf1o  27164  chtublem  27180  perfectlem2  27199  dchrfi  27224  dchrptlem1  27233  dchrptlem2  27234  dchrptlem3  27235  dchrsum2  27237  bposlem1  27253  bposlem3  27255  2sqlem5  27391  2sqlem6  27392  2sqlem8  27395  2sqlem10  27397  2sqb  27401  chebbnd1lem1  27438  chtppilimlem2  27443  dchrisum0flb  27479  dchrisum0fno1  27480  dchrisum0  27489  pntrsumbnd2  27536  pntpbnd1  27555  pntpbnd2  27556  pntlemp  27579  pnt3  27581  qabvle  27594  ostth2lem2  27603  ostth3  27607  ostth  27608  nolt02o  27665  nogt01o  27666  nosupprefixmo  27670  noinfprefixmo  27671  nosupbnd1lem3  27680  nosupbnd1lem4  27681  nosupbnd1lem5  27682  noinfbnd1lem3  27695  noinfbnd1lem4  27696  noinfbnd1lem5  27697  noetasuplem4  27706  noetainflem4  27710  etaslts  27791  cuteq1  27815  madebdaylemlrcut  27897  cutlt  27930  mulsuniflem  28147  bdayons  28274  addonbday  28277  om2noseqlt  28297  n0fincut  28353  bdaypw2n0bndlem  28461  bdayfinbndlem1  28465  z12sge0  28481  readdscl  28497  remulscl  28500  colinearalglem4  28984  axcontlem10  29048  upgrex  29167  smcnlem  30774  ubthlem1  30947  ubthlem3  30949  htthlem  30994  5oalem6  31736  leopmuli  32210  pjnormssi  32245  pjclem4  32276  pj3si  32284  hatomistici  32439  sumdmdlem  32495  sgn3da  32917  wrdt2ind  33037  xrge0tsmsd  33157  isarchiofld  33283  ordtrest2NEWlem  34081  qqhf  34145  eulerpartlemb  34527  ballotlemfc0  34652  ballotlemfcc  34653  subfacp1lem5  35380  erdszelem7  35393  erdszelem11  35397  pconnconn  35427  txpconn  35428  connpconn  35431  sconnpi1  35435  txsconn  35437  cvxsconn  35439  cvmopnlem  35474  cvmfolem  35475  cvmliftmolem2  35478  cvmliftlem7  35487  cvmliftlem10  35490  cvmlift2lem10  35508  cvmlift3lem4  35518  cvmlift3lem8  35522  satfun  35607  msubff1  35752  wzel  36018  wsuclem  36019  btwnouttr2  36218  cgrxfr  36251  btwnxfr  36252  brcolinear  36255  lineext  36272  btwnconn1lem13  36295  midofsegid  36300  segcon2  36301  brsegle  36304  seglecgr12im  36306  segletr  36310  colinbtwnle  36314  broutsideof2  36318  btwnoutside  36321  broutsideof3  36322  outsideoftr  36325  outsideofeq  36326  outsideofeu  36327  outsidele  36328  lineunray  36343  lineelsb2  36344  linethru  36349  finminlem  36514  nn0prpwlem  36518  neibastop2lem  36556  neibastop2  36557  neibastop3  36558  topjoin  36561  tailfb  36573  relowlssretop  37570  fvineqsneq  37619  wl-sbcom2d-lem1  37766  finixpnum  37808  poimirlem6  37829  poimirlem7  37830  poimirlem13  37836  poimirlem26  37849  poimirlem29  37852  heicant  37858  opnmbllem0  37859  mblfinlem3  37862  ismblfin  37864  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  itg2addnclem  37874  itg2addnclem3  37876  ftc1cnnc  37895  sdclem2  37945  fdc  37948  istotbnd3  37974  isbnd2  37986  isbnd3  37987  prdsbnd  37996  cntotbnd  37999  heibor1lem  38012  heibor1  38013  heiborlem10  38023  rrncmslem  38035  ghomco  38094  1idl  38229  unichnidl  38234  disjlem18  39081  prtlem10  39147  prtlem18  39159  atlatmstc  39601  cvrexchlem  39701  paddasslem14  40115  pexmidlem5N  40256  cdleme29ex  40656  cdlemefr29exN  40684  cdleme32fva  40719  diarnN  41411  dihlsscpre  41516  isnacs3  42973  fnwe2lem2  43314  kelac1  43326  hbtlem5  43391  hbt  43393  dgraa0p  43412  ofoafg  43617  ofoafo  43619  naddcnffo  43627  fzunt  43717  fzuntd  43718  monoordxrv  45746  rlimdmafv  47444  rlimdmafv2  47525  fmtnoprmfac2  47834  perfectALTVlem2  47989  mogoldbb  48052  lindslinindsimp2  48730