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 206  df-an 396

This theorem is referenced by:  animpimp2impd  842  3expia  1119  reximddv  3203  rexlimdvaa  3213  disjxiun  5067  wereu2  5577  frpomin  6228  ordtr3  6296  fcof1  7139  knatar  7208  riota5f  7241  ovmpodf  7407  extmptsuppeq  7975  suppss  7981  suppssOLD  7982  suppss2  7987  frrlem14  8086  fprresex  8097  wfrlem17OLD  8127  smoord  8167  tfrlem9a  8188  oaass  8354  oelimcl  8393  oaabs2  8439  swoso  8489  eceqoveq  8569  domdifsn  8795  domunsncan  8812  omxpenlem  8813  enfixsn  8821  mapdom2  8884  frfi  8989  fofinf1o  9024  finsschain  9056  elfiun  9119  marypha1lem  9122  eqsupd  9146  eqinfd  9174  ordiso2  9204  ordtypelem6  9212  ordtypelem7  9213  ordtypelem10  9216  oismo  9229  wemapsolem  9239  brwdom2  9262  wdomtr  9264  unwdomg  9273  xpwdomg  9274  unxpwdom2  9277  cantnfval2  9357  cantnfle  9359  cantnflem1  9377  cantnf  9381  r1ordg  9467  tcrank  9573  carddomi2  9659  harval2  9686  infxpenlem  9700  infxpenc2lem2  9707  fseqenlem1  9711  dfac8clem  9719  acndom2  9741  infpwfien  9749  iunfictbso  9801  dfac12lem3  9832  infxp  9902  coflim  9948  cofsmo  9956  coftr  9960  sornom  9964  infpssrlem4  9993  enfin2i  10008  fin23lem26  10012  fin23lem27  10015  fin23lem36  10035  fin23lem40  10038  isf32lem5  10044  isf34lem4  10064  isfin1-3  10073  fin1a2lem10  10096  fin1a2lem13  10099  fin1a2s  10101  hsmexlem4  10116  ttukeylem5  10200  ttukeylem6  10201  ttukeylem7  10202  alephval2  10259  gchor  10314  fpwwe2lem6  10323  fpwwe2lem11  10328  fpwwe2  10330  pwfseqlem4a  10348  pwfseqlem4  10349  winalim2  10383  gchina  10386  inar1  10462  nqereq  10622  prlem934  10720  prlem936  10734  addsrmo  10760  mulsrmo  10761  supsrlem  10798  axpre-sup  10856  dedekind  11068  dedekindle  11069  mulge0b  11775  supaddc  11872  supmul1  11874  un0addcl  12196  un0mulcl  12197  uzwo3  12612  qbtwnre  12862  xlemul1a  12951  seqcl2  13669  seqfveq2  13673  seqshft2  13677  monoord  13681  seqsplit  13684  seqf1olem1  13690  seqid2  13697  seqhomo  13698  expnegz  13745  expcan  13815  ltexp2  13816  discr  13883  bcval5  13960  hashbc  14093  hashf1lem2  14098  seqcoll  14106  seqcoll2  14107  wrdind  14363  wrd2ind  14364  cau3lem  14994  ello1d  15160  lo1bdd2  15161  rlimclim  15183  climrlim2  15184  rlimdm  15188  rlimcn1  15225  reccn2  15234  rlimsqzlem  15288  lo1le  15291  caucvgrlem  15312  caurcvg2  15317  summolem2  15356  zsum  15358  fsum  15360  fsumf1o  15363  sumss  15364  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  fsumcom2  15414  fsum0diag2  15423  fsummulc2  15424  fsumconst  15430  fsumrelem  15447  fsumrlim  15451  fsumo1  15452  divrcnv  15492  geomulcvg  15516  mertenslem2  15525  prodmolem2  15573  zprod  15575  fprod  15579  fprodf1o  15584  prodss  15585  fprodss  15586  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodconst  15616  fprodn0  15617  fprodcom2  15622  ruclem8  15874  dvds0lem  15904  dvdsnegb  15911  dvdssub2  15938  bitsf1  16081  bitsshft  16110  bezoutlem3  16177  bezoutlem4  16178  isprm5  16340  isprm6  16347  hashgcdeq  16418  modprminv  16428  modprminveq  16429  reumodprminv  16433  pcqmul  16482  pcqcl  16485  pcxnn0cl  16489  pcxcl  16490  pc2dvds  16508  pcadd  16518  pcmpt  16521  pockthg  16535  infpnlem1  16539  prmreclem5  16549  vdwlem2  16611  vdwlem9  16618  vdwlem10  16619  vdwlem12  16621  ramub  16642  0ram  16649  ramub1lem2  16656  ramub1  16657  ramcl  16658  mreexexd  17274  acsfn2  17289  iscatd  17299  catpropd  17335  setcmon  17718  pleval2i  17969  psss  18213  mgmidsssn0  18271  mhmeql  18379  frmdss2  18417  frmdup3  18421  grprcan  18528  dfgrp3lem  18588  mulgnn0ass  18654  isnsg3  18703  ghmpreima  18771  ghmeql  18772  gaorber  18829  f1omvdco2  18971  psgnunilem1  19016  psgnunilem2  19018  oddvds  19070  gexdvds  19104  sylow1lem1  19118  odcau  19124  pgpssslw  19134  sylow2alem2  19138  sylow2blem3  19142  fislw  19145  lsmmod  19196  efgredlem  19268  frgpup3  19299  gsumval3  19423  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  gsum2d2lem  19489  ablfac1eulem  19590  pgpfac1lem5  19597  ablfaclem3  19605  issubdrg  19964  lss1d  20140  lmhmeql  20232  lspextmo  20233  lspsnat  20322  lsppratlem6  20329  islbs3  20332  lbsextlem4  20338  lidl1el  20402  cnsubrg  20570  gsumfsum  20577  prmirredlem  20606  znidomb  20681  frgpcyg  20693  cssmre  20810  dsmmsubg  20860  dsmmlss  20861  frlmsslsp  20913  lindff1  20937  lindfrn  20938  rnasclassa  21009  mvrf1  21104  mplsubglem  21115  mpllsslem  21116  mplcoe1  21148  mplcoe5  21151  gsummoncoe1  21385  mat1dimcrng  21534  mdetdiaglem  21655  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  cpmatacl  21773  cpmatmcllem  21775  mp2pm2mplem4  21866  en2top  22043  toponmre  22152  topssnei  22183  innei  22184  clslp  22207  restcls  22240  restntr  22241  ordtrest2lem  22262  cnpco  22326  cncls2  22332  cncnpi  22337  cncnp  22339  cnconst2  22342  cnpdis  22352  lmcnp  22363  cnhaus  22413  isreg2  22436  cncmp  22451  tgcmp  22460  sscmp  22464  cmpfi  22467  cnconn  22481  iunconnlem  22486  clsconn  22489  1stcfb  22504  1stcrest  22512  2ndcctbss  22514  2ndcdisj  22515  1stcelcls  22520  1stccnp  22521  restnlly  22541  cldllycmp  22554  lly1stc  22555  dislly  22556  locfincmp  22585  comppfsc  22591  kgentopon  22597  kgenidm  22606  1stckgenlem  22612  kgencn3  22617  ptpjpre1  22630  ptbasin  22636  txcls  22663  tx2cn  22669  ptpjcn  22670  ptclsg  22674  ptcnp  22681  txdis  22691  txlly  22695  txnlly  22696  pthaus  22697  txtube  22699  txcmplem1  22700  txcmplem2  22701  txcmp  22702  txhaus  22706  txkgen  22711  xkohaus  22712  xkococnlem  22718  xkococn  22719  txconn  22748  qtopeu  22775  qtoprest  22776  regr1lem2  22799  kqreglem1  22800  cmphaushmeo  22859  xkocnv  22873  fgabs  22938  filuni  22944  trufil  22969  ufileu  22978  filufint  22979  fin1aufil  22991  elfm2  23007  rnelfmlem  23011  fmfnfmlem2  23014  fmfnfmlem4  23016  fmufil  23018  flimopn  23034  fbflim2  23036  hausflimi  23039  hausflim  23040  flimcf  23041  flimclslem  23043  flimsncls  23045  hauspwpwf1  23046  cnpflfi  23058  fclsnei  23078  fclscf  23084  flimfnfcls  23087  fclscmp  23089  ufilcmp  23091  fcfnei  23094  cnpfcf  23100  alexsublem  23103  alexsub  23104  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem4  23114  ptcmplem5  23115  symgtgp  23165  tgpconncompeqg  23171  tgpconncomp  23172  ghmcnp  23174  tgpt0  23178  qustgplem  23180  haustsms2  23196  tsmsgsum  23198  tsmsres  23203  tsmsxp  23214  imasdsf1olem  23434  xbln0  23475  blssps  23485  blss  23486  neibl  23563  blcld  23567  metss  23570  metequiv2  23572  met1stc  23583  metrest  23586  prdsxmslem2  23591  metcnp3  23602  nrmmetd  23636  nlmvscnlem1  23756  nrginvrcnlem  23761  nmoleub  23801  icccmplem2  23892  icccmp  23894  reconnlem2  23896  xrge0tsms  23903  metdstri  23920  metdseq0  23923  metdscn  23925  cnmpopc  23997  lebnumlem3  24032  pcoval2  24085  pcopt  24091  nmoleub2lem  24183  nmhmcn  24189  ipcnlem1  24314  cfilfcls  24343  cmetcaulem  24357  iscmet3lem2  24361  iscmet3  24362  equivcau  24369  caubl  24377  bcthlem2  24394  bcthlem3  24395  bcthlem4  24396  bcthlem5  24397  ivthlem2  24521  ivthlem3  24522  ovoliunlem2  24572  ovolicc2lem2  24587  ovolicc2lem5  24590  ovolicc2  24591  ismbl2  24596  nulmbl  24604  nulmbl2  24605  unmbl  24606  shftmbl  24607  voliunlem3  24621  volsup  24625  ioombl1lem4  24630  ioombl1  24631  icombl  24633  ioombl  24634  uniioombl  24658  opnmbllem  24670  volivth  24676  vitali  24682  mbflimsup  24735  i1fadd  24764  itg1addlem4  24768  itg1addlem4OLD  24769  itg2le  24809  itg2seq  24812  itg2lea  24814  itg2splitlem  24818  itg2split  24819  itg2mono  24823  itg2gt0  24830  itg2cnlem2  24832  itgss  24881  itgfsum  24896  itgcn  24914  ellimc3  24948  limcco  24962  limciun  24963  dvnres  25000  dvnfre  25021  rolle  25059  c1liplem1  25065  dvivth  25079  dvne0  25080  lhop1lem  25082  lhop1  25083  lhop  25085  dvcnvrelem1  25086  dvfsumrlim  25100  dvfsum2  25103  ftc1a  25106  ftc1lem6  25110  itgsubst  25118  tdeglem4  25129  tdeglem4OLD  25130  mdegaddle  25144  mdegvscale  25145  mdegmullem  25148  deg1tmle  25187  ply1divex  25206  dvdsq1p  25230  fta1g  25237  fta1b  25239  plyco0  25258  coeeulem  25290  dgrlem  25295  plyco  25307  coemullem  25316  dgreq0  25331  dgrco  25341  plydivex  25362  quotcan  25374  aannenlem1  25393  aalioulem2  25398  aalioulem3  25399  taylthlem1  25437  ulmbdd  25462  itgulm  25472  radcnvlt1  25482  psercnlem1  25489  abelthlem2  25496  abelthlem8  25503  logcnlem5  25706  efopn  25718  cxpmul2z  25751  cxpcn3lem  25805  cxpeq  25815  xrlimcnp  26023  cxplim  26026  o1cxp  26029  cxploglim  26032  scvxcvx  26040  jensen  26043  ftalem1  26127  ftalem2  26128  fta  26134  basellem3  26137  isppw2  26169  ppinprm  26206  chtnprm  26208  dvdsmulf1o  26248  chtublem  26264  perfectlem2  26283  dchrfi  26308  dchrptlem1  26317  dchrptlem2  26318  dchrptlem3  26319  dchrsum2  26321  bposlem1  26337  bposlem3  26339  2sqlem5  26475  2sqlem6  26476  2sqlem8  26479  2sqlem10  26481  2sqb  26485  chebbnd1lem1  26522  chtppilimlem2  26527  dchrisum0flb  26563  dchrisum0fno1  26564  dchrisum0  26573  pntrsumbnd2  26620  pntpbnd1  26639  pntpbnd2  26640  pntlemp  26663  pnt3  26665  qabvle  26678  ostth2lem2  26687  ostth3  26691  ostth  26692  colinearalglem4  27180  axcontlem10  27244  upgrex  27365  smcnlem  28960  ubthlem1  29133  ubthlem3  29135  htthlem  29180  5oalem6  29922  leopmuli  30396  pjnormssi  30431  pjclem4  30462  pj3si  30470  hatomistici  30625  sumdmdlem  30681  wrdt2ind  31127  xrge0tsmsd  31219  isarchiofld  31418  ordtrest2NEWlem  31774  qqhf  31836  eulerpartlemb  32235  ballotlemfc0  32359  ballotlemfcc  32360  sgn3da  32408  subfacp1lem5  33046  erdszelem7  33059  erdszelem11  33063  pconnconn  33093  txpconn  33094  connpconn  33097  sconnpi1  33101  txsconn  33103  cvxsconn  33105  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem2  33144  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift2lem10  33174  cvmlift3lem4  33184  cvmlift3lem8  33188  satfun  33273  msubff1  33418  wzel  33745  wsuclem  33746  naddssim  33764  nolt02o  33825  nogt01o  33826  nosupprefixmo  33830  noinfprefixmo  33831  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noetasuplem4  33866  noetainflem4  33870  etasslt  33934  madebdaylemlrcut  34006  btwnouttr2  34251  cgrxfr  34284  btwnxfr  34285  brcolinear  34288  lineext  34305  btwnconn1lem13  34328  midofsegid  34333  segcon2  34334  brsegle  34337  seglecgr12im  34339  segletr  34343  colinbtwnle  34347  broutsideof2  34351  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  outsideofeq  34359  outsideofeu  34360  outsidele  34361  lineunray  34376  lineelsb2  34377  linethru  34382  finminlem  34434  nn0prpwlem  34438  neibastop2lem  34476  neibastop2  34477  neibastop3  34478  topjoin  34481  tailfb  34493  relowlssretop  35461  fvineqsneq  35510  wl-sbcom2d-lem1  35641  finixpnum  35689  poimirlem6  35710  poimirlem7  35711  poimirlem13  35717  poimirlem26  35730  poimirlem29  35733  heicant  35739  opnmbllem0  35740  mblfinlem3  35743  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  itg2addnclem3  35757  ftc1cnnc  35776  sdclem2  35827  fdc  35830  istotbnd3  35856  isbnd2  35868  isbnd3  35869  prdsbnd  35878  cntotbnd  35881  heibor1lem  35894  heibor1  35895  heiborlem10  35905  rrncmslem  35917  ghomco  35976  1idl  36111  unichnidl  36116  prtlem10  36806  prtlem18  36818  atlatmstc  37260  cvrexchlem  37360  paddasslem14  37774  pexmidlem5N  37915  cdleme29ex  38315  cdlemefr29exN  38343  cdleme32fva  38378  diarnN  39070  dihlsscpre  39175  isnacs3  40448  fnwe2lem2  40792  kelac1  40804  hbtlem5  40869  hbt  40871  dgraa0p  40890  monoordxrv  42912  rlimdmafv  44556  rlimdmafv2  44637  fmtnoprmfac2  44907  perfectALTVlem2  45062  mogoldbb  45125  mgmhmeql  45245  lindslinindsimp2  45692