Theorem expr 462

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 426	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 412	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  animpimp2impd  860  3expia  1139  rexlimdvaa  3169  reximddv  3183  disjxiun  5108  wereu2  5660  frpomin  6345  ordtr3  6411  fcof1  7294  knatar  7366  riota5f  7404  ovmpodf  7575  extmptsuppeq  8190  suppss  8196  suppss2  8202  frrlem14  8302  fprresex  8313  smoord  8358  tfrlem9a  8379  oaass  8552  oelimcl  8592  oaabs2  8641  cofon1  8664  naddssim  8678  swoso  8735  eceqoveq  8826  domdifsn  9055  domunsncan  9072  omxpenlem  9073  enfixsn  9081  mapdom2  9143  frfi  9252  fofinf1o  9296  finsschain  9323  elfiun  9397  marypha1lem  9400  eqsupd  9424  eqinfd  9453  ordiso2  9484  ordtypelem6  9492  ordtypelem7  9493  ordtypelem10  9496  oismo  9509  wemapsolem  9519  brwdom2  9542  wdomtr  9544  unwdomg  9553  xpwdomg  9554  unxpwdom2  9557  cantnfval2  9645  cantnfle  9647  cantnflem1  9665  cantnf  9669  r1ordg  9757  tcrank  9863  carddomi2  9972  harval2  9999  infxpenlem  10013  infxpenc2lem2  10020  fseqenlem1  10024  dfac8clem  10032  acndom2  10054  infpwfien  10062  iunfictbso  10114  dfac12lem3  10145  infxp  10213  coflim  10260  cofsmo  10268  coftr  10272  sornom  10276  infpssrlem4  10305  enfin2i  10320  fin23lem26  10324  fin23lem27  10327  fin23lem36  10347  fin23lem40  10350  isf32lem5  10356  isf34lem4  10376  isfin1-3  10385  fin1a2lem10  10408  fin1a2lem13  10411  fin1a2s  10413  hsmexlem4  10428  ttukeylem5  10512  ttukeylem6  10513  ttukeylem7  10514  alephval2  10576  gchor  10631  fpwwe2lem6  10640  fpwwe2lem11  10645  fpwwe2  10647  pwfseqlem4a  10665  pwfseqlem4  10666  winalim2  10700  gchina  10703  inar1  10779  nqereq  10939  prlem934  11037  prlem936  11051  addsrmo  11077  mulsrmo  11078  supsrlem  11115  axpre-sup  11173  dedekind  11392  dedekindle  11393  mulge0b  12104  supaddc  12201  supmul1  12203  un0addcl  12556  un0mulcl  12557  uzwo3  12987  qbtwnre  13245  xlemul1a  13334  seqcl2  14078  seqfveq2  14082  seqshft2  14086  monoord  14090  seqsplit  14093  seqf1olem1  14099  seqid2  14106  seqhomo  14107  expnegz  14154  expcan  14227  ltexp2  14228  discr  14298  bcval5  14376  hashbc  14512  hashf1lem2  14515  seqcoll  14523  seqcoll2  14524  wrdind  14785  wrd2ind  14786  sgn3da  15166  cau3lem  15434  ello1d  15602  lo1bdd2  15603  rlimclim  15625  climrlim2  15626  rlimdm  15630  rlimcn1  15667  reccn2  15676  rlimsqzlem  15728  lo1le  15731  caucvgrlem  15752  caurcvg2  15757  summolem2  15794  zsum  15796  fsum  15798  fsumf1o  15801  sumss  15802  fsumss  15803  fsumcl2lem  15809  fsumadd  15818  fsumcom2  15852  fsum0diag2  15861  fsummulc2  15862  fsumconst  15868  fsumrelem  15886  fsumrlim  15890  fsumo1  15891  divrcnv  15933  geomulcvg  15957  mertenslem2  15966  prodmolem2  16016  zprod  16018  fprod  16022  fprodf1o  16027  prodss  16028  fprodss  16029  fprodcl2lem  16031  fprodmul  16041  fproddiv  16042  fprodconst  16059  fprodn0  16060  fprodcom2  16065  ruclem8  16319  dvds0lem  16350  dvdsnegb  16357  dvdssub2  16385  bitsf1  16530  bitsshft  16559  bezoutlem3  16625  bezoutlem4  16626  isprm5  16792  isprm6  16799  hashgcdeq  16875  modprminv  16885  modprminveq  16886  reumodprminv  16890  pcqmul  16939  pcqcl  16942  pcxnn0cl  16946  pcxcl  16947  pc2dvds  16965  pcadd  16975  pcmpt  16978  pockthg  16992  infpnlem1  16996  prmreclem5  17006  vdwlem2  17068  vdwlem9  17075  vdwlem10  17076  vdwlem12  17078  ramub  17099  0ram  17106  ramub1lem2  17113  ramub1  17114  ramcl  17115  mreexexd  17730  acsfn2  17745  iscatd  17755  catpropd  17791  setcmon  18170  pleval2i  18416  psss  18662  mgmidsssn0  18760  mgmhmeql  18810  mhmeql  18926  frmdss2  18963  frmdup3  18967  grprcan  19088  dfgrp3lem  19152  mulgnn0ass  19224  isnsg3  19274  ghmpreima  19356  ghmeql  19357  gaorber  19426  f1omvdco2  19566  psgnunilem1  19611  psgnunilem2  19613  oddvds  19665  gexdvds  19702  sylow1lem1  19716  odcau  19722  pgpssslw  19732  sylow2alem2  19736  sylow2blem3  19740  fislw  19743  lsmmod  19793  efgredlem  19865  frgpup3  19896  gsumval3  20025  gsumzres  20027  gsumzcl2  20028  gsumzf1o  20030  gsumzaddlem  20039  gsumconst  20052  gsumzmhm  20055  gsumzoppg  20062  gsum2d2lem  20091  ablfac1eulem  20192  pgpfac1lem5  20199  ablfaclem3  20207  issubdrg  20937  lss1d  21138  lmhmeql  21230  lspextmo  21231  lspsnat  21323  lsppratlem6  21330  islbs3  21333  lbsextlem4  21339  lidl1el  21405  cnsubrg  21631  gsumfsum  21638  prmirredlem  21676  znidomb  21765  frgpcyg  21777  cssmre  21897  dsmmsubg  21947  dsmmlss  21948  frlmsslsp  22000  lindff1  22024  lindfrn  22025  rnasclassa  22099  mvrf1  22189  mplsubglem  22202  mpllsslem  22203  mplcoe1  22242  mplcoe5  22245  gsummoncoe1  22522  mat1dimcrng  22688  mdetdiaglem  22809  mdetunilem7  22829  mdetunilem8  22830  mdetunilem9  22831  cpmatacl  22927  cpmatmcllem  22929  mp2pm2mplem4  23020  en2top  23196  toponmre  23304  topssnei  23335  innei  23336  clslp  23359  restcls  23392  restntr  23393  ordtrest2lem  23414  cnpco  23478  cncls2  23484  cncnpi  23489  cncnp  23491  cnconst2  23494  cnpdis  23504  lmcnp  23515  cnhaus  23565  isreg2  23588  cncmp  23603  tgcmp  23612  sscmp  23616  cmpfi  23619  cnconn  23633  iunconnlem  23638  clsconn  23641  1stcfb  23656  1stcrest  23664  2ndcctbss  23667  2ndcdisj  23668  1stcelcls  23673  1stccnp  23674  restnlly  23694  cldllycmp  23707  lly1stc  23708  dislly  23709  locfincmp  23738  comppfsc  23744  kgentopon  23750  kgenidm  23759  1stckgenlem  23765  kgencn3  23770  ptpjpre1  23783  ptbasin  23789  txcls  23816  tx2cn  23822  ptpjcn  23823  ptclsg  23827  ptcnp  23834  txdis  23844  txlly  23848  txnlly  23849  pthaus  23850  txtube  23852  txcmplem1  23853  txcmplem2  23854  txcmp  23855  txhaus  23859  txkgen  23864  xkohaus  23865  xkococnlem  23871  xkococn  23872  txconn  23901  qtopeu  23928  qtoprest  23929  regr1lem2  23952  kqreglem1  23953  cmphaushmeo  24012  xkocnv  24026  fgabs  24091  filuni  24097  trufil  24122  ufileu  24131  filufint  24132  fin1aufil  24144  elfm2  24160  rnelfmlem  24164  fmfnfmlem2  24167  fmfnfmlem4  24169  fmufil  24171  flimopn  24187  fbflim2  24189  hausflimi  24192  hausflim  24193  flimcf  24194  flimclslem  24196  flimsncls  24198  hauspwpwf1  24199  cnpflfi  24211  fclsnei  24231  fclscf  24237  flimfnfcls  24240  fclscmp  24242  ufilcmp  24244  fcfnei  24247  cnpfcf  24253  alexsublem  24256  alexsub  24257  alexsubALTlem2  24260  alexsubALTlem3  24261  alexsubALTlem4  24262  ptcmplem3  24266  ptcmplem4  24267  ptcmplem5  24268  symgtgp  24318  tgpconncompeqg  24324  tgpconncomp  24325  ghmcnp  24327  tgpt0  24331  qustgplem  24333  haustsms2  24349  tsmsgsum  24351  tsmsres  24356  tsmsxp  24367  imasdsf1olem  24585  xbln0  24626  blssps  24636  blss  24637  neibl  24713  blcld  24717  metss  24720  metequiv2  24722  met1stc  24733  metrest  24736  prdsxmslem2  24741  metcnp3  24752  nrmmetd  24786  nlmvscnlem1  24898  nrginvrcnlem  24903  nmoleub  24943  icccmplem2  25036  icccmp  25038  reconnlem2  25040  xrge0tsms  25047  metdstri  25064  metdseq0  25067  metdscn  25069  cnmpopc  25142  lebnumlem3  25177  pcoval2  25230  pcopt  25236  nmoleub2lem  25328  nmhmcn  25334  ipcnlem1  25459  cfilfcls  25488  cmetcaulem  25502  iscmet3lem2  25506  iscmet3  25507  equivcau  25514  caubl  25522  bcthlem2  25539  bcthlem3  25540  bcthlem4  25541  bcthlem5  25542  ivthlem2  25666  ivthlem3  25667  ovoliunlem2  25717  ovolicc2lem2  25732  ovolicc2lem5  25735  ovolicc2  25736  ismbl2  25741  nulmbl  25749  nulmbl2  25750  unmbl  25751  shftmbl  25752  voliunlem3  25766  volsup  25770  ioombl1lem4  25775  ioombl1  25776  icombl  25778  ioombl  25779  uniioombl  25803  opnmbllem  25815  volivth  25821  vitali  25827  mbflimsup  25880  i1fadd  25909  itg1addlem4  25913  itg2le  25953  itg2seq  25956  itg2lea  25958  itg2splitlem  25962  itg2split  25963  itg2mono  25967  itg2gt0  25974  itg2cnlem2  25976  itgss  26026  itgfsum  26041  itgcn  26059  ellimc3  26093  limcco  26107  limciun  26108  dvnres  26145  dvnfre  26166  rolle  26204  c1liplem1  26210  dvivth  26224  dvne0  26225  lhop1lem  26227  lhop1  26228  lhop  26230  dvcnvrelem1  26231  dvfsumrlim  26245  dvfsum2  26248  ftc1a  26251  ftc1lem6  26255  itgsubst  26263  tdeglem4  26272  mdegaddle  26286  mdegvscale  26287  mdegmullem  26290  deg1tmle  26330  ply1divex  26349  dvdsq1p  26375  fta1g  26382  fta1b  26384  plyco0  26404  coeeulem  26436  dgrlem  26441  plyco  26453  coemullem  26462  dgreq0  26477  dgrco  26487  plydivex  26513  quotcan  26525  aannenlem1  26546  aalioulem2  26551  aalioulem3  26552  taylthlem1  26591  ulmbdd  26616  itgulm  26626  radcnvlt1  26636  psercnlem1  26643  abelthlem2  26650  abelthlem8  26657  logcnlem5  26866  efopn  26878  cxpmul2z  26911  cxpcn3lem  26967  cxpeq  26977  xrlimcnp  27188  cxplim  27191  o1cxp  27194  cxploglim  27197  scvxcvx  27205  jensen  27208  ftalem1  27292  ftalem2  27293  fta  27299  basellem3  27302  isppw2  27334  ppinprm  27371  chtnprm  27373  mpodvdsmulf1o  27413  dvdsmulf1o  27415  chtublem  27430  perfectlem2  27449  dchrfi  27474  dchrptlem1  27483  dchrptlem2  27484  dchrptlem3  27485  dchrsum2  27487  bposlem1  27503  bposlem3  27505  2sqlem5  27641  2sqlem6  27642  2sqlem8  27645  2sqlem10  27647  2sqb  27651  chebbnd1lem1  27688  chtppilimlem2  27693  dchrisum0flb  27729  dchrisum0fno1  27730  dchrisum0  27739  pntrsumbnd2  27786  pntpbnd1  27805  pntpbnd2  27806  pntlemp  27829  pnt3  27831  qabvle  27844  ostth2lem2  27853  ostth3  27857  ostth  27858  nolt02o  27914  nogt01o  27915  nosupprefixmo  27919  noinfprefixmo  27920  nosupbnd1lem3  27929  nosupbnd1lem4  27930  nosupbnd1lem5  27931  noinfbnd1lem3  27944  noinfbnd1lem4  27945  noinfbnd1lem5  27946  noetasuplem4  27955  noetainflem4  27959  etaslts  28041  cuteq1  28065  madebdaylemlrcut  28147  cutlt  28180  mulsuniflem  28397  bdayons  28524  addonbday  28527  om2noseqlt  28547  n0fincut  28603  bdaypw2n0bndlem  28711  bdayfinbndlem1  28715  z12sge0  28731  readdscl  28747  remulscl  28750  colinearalglem4  29318  axcontlem10  29382  upgrex  29501  smcnlem  31124  ubthlem1  31297  ubthlem3  31299  htthlem  31344  5oalem6  32086  leopmuli  32560  pjnormssi  32595  pjclem4  32626  pj3si  32634  hatomistici  32789  sumdmdlem  32845  wrdt2ind  33343  xrge0tsmsd  33461  isarchiofld  33587  ordtrest2NEWlem  34380  qqhf  34444  eulerpartlemb  34827  ballotlemfc0  34952  ballotlemfcc  34953  subfacp1lem5  35717  erdszelem7  35730  erdszelem11  35734  pconnconn  35764  txpconn  35765  connpconn  35768  sconnpi1  35772  txsconn  35774  cvxsconn  35776  cvmopnlem  35811  cvmfolem  35812  cvmliftmolem2  35815  cvmliftlem7  35824  cvmliftlem10  35827  cvmlift2lem10  35845  cvmlift3lem4  35855  cvmlift3lem8  35859  satfun  35944  msubff1  36089  wzel  36355  wsuclem  36356  btwnouttr2  36555  cgrxfr  36588  btwnxfr  36589  brcolinear  36592  lineext  36609  btwnconn1lem13  36632  midofsegid  36637  segcon2  36638  brsegle  36641  seglecgr12im  36643  segletr  36647  colinbtwnle  36651  broutsideof2  36655  btwnoutside  36658  broutsideof3  36659  outsideoftr  36662  outsideofeq  36663  outsideofeu  36664  outsidele  36665  lineunray  36680  lineelsb2  36681  linethru  36686  nmulrid  36730  nmuladdss  36746  nadddilem1  36753  finminlem  36890  nn0prpwlem  36894  neibastop2lem  36932  neibastop2  36933  neibastop3  36934  topjoin  36937  tailfb  36949  axtcond  37050  relowlssretop  38070  fvineqsneq  38119  wl-sbcom2d-lem1  38275  finixpnum  38317  poimirlem6  38338  poimirlem7  38339  poimirlem13  38345  poimirlem26  38358  poimirlem29  38361  heicant  38367  opnmbllem0  38368  mblfinlem3  38371  ismblfin  38373  ovoliunnfl  38374  voliunnfl  38376  volsupnfl  38377  itg2addnclem  38383  itg2addnclem3  38385  ftc1cnnc  38404  sdclem2  38455  fdc  38458  istotbnd3  38484  isbnd2  38496  isbnd3  38497  prdsbnd  38506  cntotbnd  38509  heibor1lem  38522  heibor1  38523  heiborlem10  38533  rrncmslem  38545  ghomco  38604  1idl  38739  unichnidl  38744  disjlem18  39614  prtlem10  39701  prtlem18  39713  atlatmstc  40155  cvrexchlem  40255  paddasslem14  40669  pexmidlem5N  40810  cdleme29ex  41210  cdlemefr29exN  41238  cdleme32fva  41273  diarnN  41965  dihlsscpre  42070  isnacs3  43518  fnwe2lem2  43855  kelac1  43867  hbtlem5  43932  hbt  43934  dgraa0p  43953  ofoafg  44158  ofoafo  44160  naddcnffo  44168  fzunt  44258  fzuntd  44259  monoordxrv  46272  rlimdmafv  47991  rlimdmafv2  48072  fmtnoprmfac2  48396  perfectALTVlem2  48564  mogoldbb  48627  lindslinindsimp2  49319