Theorem expr 643

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
expr	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 631	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 445	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  reximddv  3018  rexlimdvaa  3032  disjxiun  4649  disjxiunOLD  4650  wereu2  5111  ordtr3  5769  fcof1  6542  knatar  6607  riota5f  6636  ovmpt2df  6792  extmptsuppeq  7319  suppss  7325  suppss2  7329  wfrlem17  7431  smoord  7462  tfrlem9a  7482  oaass  7641  oelimcl  7680  oaabs2  7725  swoso  7775  eceqoveq  7853  domdifsn  8043  domunsncan  8060  omxpenlem  8061  enfixsn  8069  mapdom2  8131  frfi  8205  fofinf1o  8241  finsschain  8273  elfiun  8336  marypha1lem  8339  eqsupd  8363  eqinfd  8391  ordiso2  8420  ordtypelem6  8428  ordtypelem7  8429  ordtypelem10  8432  oismo  8445  wemapsolem  8455  brwdom2  8478  wdomtr  8480  unwdomg  8489  xpwdomg  8490  unxpwdom2  8493  cantnfval2  8566  cantnfle  8568  cantnflem1  8586  cantnf  8590  r1ordg  8641  tcrank  8747  carddomi2  8796  harval2  8823  infxpenlem  8836  infxpenc2lem2  8843  fseqenlem1  8847  dfac8clem  8855  acndom2  8877  infpwfien  8885  iunfictbso  8937  dfac12lem3  8967  infxp  9037  coflim  9083  cofsmo  9091  coftr  9095  sornom  9099  infpssrlem4  9128  enfin2i  9143  fin23lem26  9147  fin23lem27  9150  fin23lem36  9170  fin23lem40  9173  isf32lem5  9179  isf34lem4  9199  isfin1-3  9208  fin1a2lem10  9231  fin1a2lem13  9234  fin1a2s  9236  hsmexlem4  9251  ttukeylem5  9335  ttukeylem6  9336  ttukeylem7  9337  alephval2  9394  gchor  9449  fpwwe2lem7  9458  fpwwe2lem12  9463  fpwwe2  9465  pwfseqlem4a  9483  pwfseqlem4  9484  winalim2  9518  gchina  9521  inar1  9597  nqereq  9757  prlem934  9855  prlem936  9869  addsrmo  9894  mulsrmo  9895  supsrlem  9932  axpre-sup  9990  dedekind  10200  dedekindle  10201  prodge0  10870  mulge0b  10893  supaddc  10990  supmul1  10992  un0addcl  11326  un0mulcl  11327  uzwo3  11783  qbtwnre  12030  xlemul1a  12118  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqf1olem1  12840  seqid2  12847  seqhomo  12848  expnegz  12894  expcan  12913  ltexp2  12914  discr  13001  bcval5  13105  hashbc  13237  hashf1lem2  13240  seqcoll  13248  seqcoll2  13249  wrdind  13476  wrd2ind  13477  cau3lem  14094  ello1d  14254  lo1bdd2  14255  rlimclim  14277  climrlim2  14278  rlimdm  14282  rlimcn1  14319  reccn2  14327  rlimsqzlem  14379  lo1le  14382  caucvgrlem  14403  caurcvg2  14408  summolem2  14447  zsum  14449  fsum  14451  fsumf1o  14454  sumss  14455  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  fsumcom2  14505  fsumcom2OLD  14506  fsum0diag2  14515  fsummulc2  14516  fsumconst  14522  fsumrelem  14539  fsumrlim  14543  fsumo1  14544  divrcnv  14584  geomulcvg  14607  mertenslem2  14617  prodmolem2  14665  zprod  14667  fprod  14671  fprodf1o  14676  prodss  14677  fprodss  14678  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodconst  14708  fprodn0  14709  fprodcom2  14714  fprodcom2OLD  14715  ruclem8  14966  dvds0lem  14992  dvdsnegb  14999  dvdssub2  15023  bitsf1  15168  bitsshft  15197  bezoutlem3  15258  bezoutlem4  15259  isprm5  15419  isprm6  15426  hashgcdeq  15494  modprminv  15504  modprminveq  15505  reumodprminv  15509  pcqmul  15558  pcqcl  15561  pcxcl  15565  pc2dvds  15583  pcadd  15593  pcmpt  15596  pockthg  15610  infpnlem1  15614  prmreclem5  15624  vdwlem2  15686  vdwlem9  15693  vdwlem10  15694  vdwlem12  15696  ramub  15717  0ram  15724  ramub1lem2  15731  ramub1  15732  ramcl  15733  mreexexd  16308  mreexexdOLD  16309  acsfn2  16324  iscatd  16334  catpropd  16369  setcmon  16737  pleval2i  16964  psss  17214  mgmidsssn0  17269  mhmeql  17364  frmdss2  17400  frmdup3  17404  grprcan  17455  dfgrp3lem  17513  mulgnn0ass  17578  isnsg3  17628  ghmpreima  17682  ghmeql  17683  gaorber  17741  f1omvdco2  17868  psgnunilem1  17913  psgnunilem2  17915  oddvds  17966  gexdvds  17999  sylow1lem1  18013  odcau  18019  pgpssslw  18029  sylow2alem2  18033  sylow2blem3  18037  fislw  18040  lsmmod  18088  efgredlem  18160  frgpup3  18191  gsumval3  18308  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  gsum2d2lem  18372  ablfac1eulem  18471  pgpfac1lem5  18478  ablfaclem3  18486  issubdrg  18805  lss1d  18963  lmhmeql  19055  lspextmo  19056  lspsnat  19145  lsppratlem6  19152  islbs3  19155  lbsextlem4  19161  lidl1el  19218  mvrf1  19425  mplsubglem  19434  mpllsslem  19435  mplcoe1  19465  mplcoe5  19468  gsummoncoe1  19674  cnsubrg  19806  gsumfsum  19813  prmirredlem  19841  znidomb  19910  frgpcyg  19922  cssmre  20037  dsmmsubg  20087  dsmmlss  20088  frlmsslsp  20135  lindff1  20159  lindfrn  20160  mat1dimcrng  20283  mdetdiaglem  20404  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  cpmatacl  20521  cpmatmcllem  20523  mp2pm2mplem4  20614  en2top  20789  toponmre  20897  topssnei  20928  innei  20929  clslp  20952  restcls  20985  restntr  20986  ordtrest2lem  21007  cnpco  21071  cncls2  21077  cncnpi  21082  cncnp  21084  cnconst2  21087  cnpdis  21097  lmcnp  21108  cnhaus  21158  isreg2  21181  cncmp  21195  tgcmp  21204  sscmp  21208  cmpfi  21211  cnconn  21225  iunconnlem  21230  clsconn  21233  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  2ndcdisj  21259  1stcelcls  21264  1stccnp  21265  restnlly  21285  cldllycmp  21298  lly1stc  21299  dislly  21300  locfincmp  21329  comppfsc  21335  kgentopon  21341  kgenidm  21350  1stckgenlem  21356  kgencn3  21361  ptpjpre1  21374  ptbasin  21380  txcls  21407  tx2cn  21413  ptpjcn  21414  ptclsg  21418  ptcnp  21425  txdis  21435  txlly  21439  txnlly  21440  pthaus  21441  txtube  21443  txcmplem1  21444  txcmplem2  21445  txcmp  21446  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  xkococn  21463  txconn  21492  qtopeu  21519  qtoprest  21520  regr1lem2  21543  kqreglem1  21544  cmphaushmeo  21603  xkocnv  21617  fgabs  21683  filuni  21689  trufil  21714  ufileu  21723  filufint  21724  fin1aufil  21736  elfm2  21752  rnelfmlem  21756  fmfnfmlem2  21759  fmfnfmlem4  21761  fmufil  21763  flimopn  21779  fbflim2  21781  hausflimi  21784  hausflim  21785  flimcf  21786  flimclslem  21788  flimsncls  21790  hauspwpwf1  21791  cnpflfi  21803  fclsnei  21823  fclscf  21829  flimfnfcls  21832  fclscmp  21834  ufilcmp  21836  fcfnei  21839  cnpfcf  21845  alexsublem  21848  alexsub  21849  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem4  21859  ptcmplem5  21860  symgtgp  21905  tgpconncompeqg  21915  tgpconncomp  21916  ghmcnp  21918  tgpt0  21922  qustgplem  21924  haustsms2  21940  tsmsgsum  21942  tsmsres  21947  tsmsxp  21958  imasdsf1olem  22178  xbln0  22219  blssps  22229  blss  22230  neibl  22306  blcld  22310  metss  22313  metequiv2  22315  met1stc  22326  metrest  22329  prdsxmslem2  22334  metcnp3  22345  nrmmetd  22379  nlmvscnlem1  22490  nrginvrcnlem  22495  nmoleub  22535  icccmplem2  22626  icccmp  22628  reconnlem2  22630  xrge0tsms  22637  metdstri  22654  metdseq0  22657  metdscn  22659  cnmpt2pc  22727  lebnumlem3  22762  pcoval2  22816  pcopt  22822  nmoleub2lem  22914  nmhmcn  22920  ipcnlem1  23044  cfilfcls  23072  cmetcaulem  23086  iscmet3lem2  23090  iscmet3  23091  equivcau  23098  caubl  23106  bcthlem2  23122  bcthlem3  23123  bcthlem4  23124  bcthlem5  23125  ivthlem2  23221  ivthlem3  23222  ovoliunlem2  23271  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem5  23289  ovolicc2  23290  ismbl2  23295  nulmbl  23303  nulmbl2  23304  unmbl  23305  shftmbl  23306  voliunlem3  23320  volsup  23324  ioombl1lem4  23329  ioombl1  23330  icombl  23332  ioombl  23333  uniioombl  23357  opnmbllem  23369  volivth  23375  vitali  23382  mbflimsup  23433  i1fadd  23462  itg1addlem4  23466  itg2le  23506  itg2seq  23509  itg2lea  23511  itg2splitlem  23515  itg2split  23516  itg2mono  23520  itg2gt0  23527  itg2cnlem2  23529  itgss  23578  itgfsum  23593  itgcn  23609  ellimc3  23643  limcco  23657  limciun  23658  dvnres  23694  dvnfre  23715  rolle  23753  c1liplem1  23759  dvivth  23773  dvne0  23774  lhop1lem  23776  lhop1  23777  lhop  23779  dvcnvrelem1  23780  dvfsumrlim  23794  dvfsum2  23797  ftc1a  23800  ftc1lem6  23804  itgsubst  23812  tdeglem4  23820  mdegaddle  23834  mdegvscale  23835  mdegmullem  23838  deg1tmle  23877  ply1divex  23896  dvdsq1p  23920  fta1g  23927  fta1b  23929  plyco0  23948  coeeulem  23980  dgrlem  23985  plyco  23997  coemullem  24006  dgreq0  24021  dgrco  24031  plydivex  24052  quotcan  24064  aannenlem1  24083  aalioulem2  24088  aalioulem3  24089  taylthlem1  24127  ulmbdd  24152  itgulm  24162  radcnvlt1  24172  psercnlem1  24179  abelthlem2  24186  abelthlem8  24193  logcnlem5  24392  efopn  24404  cxpmul2z  24437  cxpcn3lem  24488  cxpeq  24498  xrlimcnp  24695  cxplim  24698  o1cxp  24701  cxploglim  24704  scvxcvx  24712  jensen  24715  ftalem1  24799  ftalem2  24800  fta  24806  basellem3  24809  isppw2  24841  ppinprm  24878  chtnprm  24880  dvdsmulf1o  24920  chtublem  24936  perfectlem2  24955  dchrfi  24980  dchrptlem1  24989  dchrptlem2  24990  dchrptlem3  24991  dchrsum2  24993  bposlem1  25009  bposlem3  25011  2sqlem5  25147  2sqlem6  25148  2sqlem8  25151  2sqlem10  25153  2sqb  25157  chebbnd1lem1  25158  chtppilimlem2  25163  dchrisum0flb  25199  dchrisum0fno1  25200  dchrisum0  25209  pntrsumbnd2  25256  pntpbnd1  25275  pntpbnd2  25276  pntlemp  25299  pnt3  25301  qabvle  25314  ostth2lem2  25323  ostth3  25327  ostth  25328  colinearalglem4  25789  axcontlem10  25853  upgrex  25987  smcnlem  27552  ubthlem1  27726  ubthlem3  27728  htthlem  27774  5oalem6  28518  leopmuli  28992  pjnormssi  29027  pjclem4  29058  pj3si  29066  hatomistici  29221  sumdmdlem  29277  xrge0tsmsd  29785  isarchiofld  29817  ordtrest2NEWlem  29968  qqhf  30030  eulerpartlemb  30430  ballotlemfc0  30554  ballotlemfcc  30555  sgn3da  30603  subfacp1lem5  31166  erdszelem7  31179  erdszelem11  31183  pconnconn  31213  txpconn  31214  connpconn  31217  sconnpi1  31221  txsconn  31223  cvxsconn  31225  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem10  31294  cvmlift3lem4  31304  cvmlift3lem8  31308  msubff1  31453  wzel  31771  wzelOLD  31772  wsuclem  31773  wsuclemOLD  31774  nolt02o  31845  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  noetalem3  31865  btwnouttr2  32129  cgrxfr  32162  btwnxfr  32163  brcolinear  32166  lineext  32183  btwnconn1lem13  32206  midofsegid  32211  segcon2  32212  brsegle  32215  seglecgr12im  32217  segletr  32221  colinbtwnle  32225  broutsideof2  32229  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsideofeq  32237  outsideofeu  32238  outsidele  32239  lineunray  32254  lineelsb2  32255  linethru  32260  finminlem  32312  nn0prpwlem  32317  neibastop2lem  32355  neibastop2  32356  neibastop3  32357  topjoin  32360  tailfb  32372  relowlssretop  33211  wl-sbcom2d-lem1  33342  finixpnum  33394  poimirlem6  33415  poimirlem7  33416  poimirlem13  33422  poimirlem26  33435  poimirlem29  33438  heicant  33444  opnmbllem0  33445  mblfinlem3  33448  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  itg2addnclem3  33463  ftc1cnnc  33484  sdclem2  33538  fdc  33541  istotbnd3  33570  isbnd2  33582  isbnd3  33583  prdsbnd  33592  cntotbnd  33595  heibor1lem  33608  heibor1  33609  heiborlem10  33619  rrncmslem  33631  ghomco  33690  1idl  33825  unichnidl  33830  prtlem10  34150  prtlem18  34162  atlatmstc  34606  cvrexchlem  34705  paddasslem14  35119  pexmidlem5N  35260  cdleme29ex  35662  cdlemefr29exN  35690  cdleme32fva  35725  diarnN  36418  dihlsscpre  36523  isnacs3  37273  fnwe2lem2  37621  kelac1  37633  hbtlem5  37698  hbt  37700  dgraa0p  37719  rlimdmafv  41257  smonoord  41341  fmtnoprmfac2  41479  perfectALTVlem2  41631  mogoldbb  41673  mgmhmeql  41803  lindslinindsimp2  42252