Theorem expr 457

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  animpimp2impd  852  3expia  1127  rexlimdvaa  3141  reximddv  3155  disjxiun  5070  wereu2  5616  frpomin  6292  ordtr3  6357  fcof1  7232  knatar  7302  riota5f  7342  ovmpodf  7513  extmptsuppeq  8129  suppss  8135  suppss2  8141  frrlem14  8240  fprresex  8251  smoord  8296  tfrlem9a  8316  oaass  8487  oelimcl  8527  oaabs2  8576  cofon1  8599  naddssim  8612  swoso  8669  eceqoveq  8760  domdifsn  8989  domunsncan  9006  omxpenlem  9007  enfixsn  9015  mapdom2  9077  frfi  9186  fofinf1o  9233  finsschain  9260  elfiun  9334  marypha1lem  9337  eqsupd  9361  eqinfd  9390  ordiso2  9421  ordtypelem6  9429  ordtypelem7  9430  ordtypelem10  9433  oismo  9446  wemapsolem  9456  brwdom2  9479  wdomtr  9481  unwdomg  9490  xpwdomg  9491  unxpwdom2  9494  cantnfval2  9582  cantnfle  9584  cantnflem1  9602  cantnf  9606  r1ordg  9694  tcrank  9800  carddomi2  9886  harval2  9913  infxpenlem  9927  infxpenc2lem2  9934  fseqenlem1  9938  dfac8clem  9946  acndom2  9968  infpwfien  9976  iunfictbso  10028  dfac12lem3  10060  infxp  10128  coflim  10175  cofsmo  10183  coftr  10187  sornom  10191  infpssrlem4  10220  enfin2i  10235  fin23lem26  10239  fin23lem27  10242  fin23lem36  10262  fin23lem40  10265  isf32lem5  10271  isf34lem4  10291  isfin1-3  10300  fin1a2lem10  10323  fin1a2lem13  10326  fin1a2s  10328  hsmexlem4  10343  ttukeylem5  10427  ttukeylem6  10428  ttukeylem7  10429  alephval2  10487  gchor  10542  fpwwe2lem6  10551  fpwwe2lem11  10556  fpwwe2  10558  pwfseqlem4a  10576  pwfseqlem4  10577  winalim2  10611  gchina  10614  inar1  10690  nqereq  10850  prlem934  10948  prlem936  10962  addsrmo  10988  mulsrmo  10989  supsrlem  11026  axpre-sup  11084  dedekind  11301  dedekindle  11302  mulge0b  12018  supaddc  12115  supmul1  12117  un0addcl  12462  un0mulcl  12463  uzwo3  12885  qbtwnre  13143  xlemul1a  13232  seqcl2  13974  seqfveq2  13978  seqshft2  13982  monoord  13986  seqsplit  13989  seqf1olem1  13995  seqid2  14002  seqhomo  14003  expnegz  14050  expcan  14123  ltexp2  14124  discr  14194  bcval5  14272  hashbc  14407  hashf1lem2  14410  seqcoll  14418  seqcoll2  14419  wrdind  14676  wrd2ind  14677  cau3lem  15309  ello1d  15477  lo1bdd2  15478  rlimclim  15500  climrlim2  15501  rlimdm  15505  rlimcn1  15542  reccn2  15551  rlimsqzlem  15603  lo1le  15606  caucvgrlem  15627  caurcvg2  15632  summolem2  15670  zsum  15672  fsum  15674  fsumf1o  15677  sumss  15678  fsumss  15679  fsumcl2lem  15685  fsumadd  15694  fsumcom2  15728  fsum0diag2  15737  fsummulc2  15738  fsumconst  15744  fsumrelem  15762  fsumrlim  15766  fsumo1  15767  divrcnv  15809  geomulcvg  15833  mertenslem2  15842  prodmolem2  15892  zprod  15894  fprod  15898  fprodf1o  15903  prodss  15904  fprodss  15905  fprodcl2lem  15907  fprodmul  15917  fproddiv  15918  fprodconst  15935  fprodn0  15936  fprodcom2  15941  ruclem8  16196  dvds0lem  16227  dvdsnegb  16234  dvdssub2  16262  bitsf1  16407  bitsshft  16436  bezoutlem3  16502  bezoutlem4  16503  isprm5  16669  isprm6  16676  hashgcdeq  16752  modprminv  16762  modprminveq  16763  reumodprminv  16767  pcqmul  16816  pcqcl  16819  pcxnn0cl  16823  pcxcl  16824  pc2dvds  16842  pcadd  16852  pcmpt  16855  pockthg  16869  infpnlem1  16873  prmreclem5  16883  vdwlem2  16945  vdwlem9  16952  vdwlem10  16953  vdwlem12  16955  ramub  16976  0ram  16983  ramub1lem2  16990  ramub1  16991  ramcl  16992  mreexexd  17606  acsfn2  17621  iscatd  17631  catpropd  17667  setcmon  18046  pleval2i  18292  psss  18538  mgmidsssn0  18632  mgmhmeql  18676  mhmeql  18786  frmdss2  18823  frmdup3  18827  grprcan  18941  dfgrp3lem  19006  mulgnn0ass  19078  isnsg3  19127  ghmpreima  19205  ghmeql  19206  gaorber  19275  f1omvdco2  19415  psgnunilem1  19460  psgnunilem2  19462  oddvds  19514  gexdvds  19551  sylow1lem1  19565  odcau  19571  pgpssslw  19581  sylow2alem2  19585  sylow2blem3  19589  fislw  19592  lsmmod  19642  efgredlem  19714  frgpup3  19745  gsumval3  19874  gsumzres  19876  gsumzcl2  19877  gsumzf1o  19879  gsumzaddlem  19888  gsumconst  19901  gsumzmhm  19904  gsumzoppg  19911  gsum2d2lem  19940  ablfac1eulem  20041  pgpfac1lem5  20048  ablfaclem3  20056  issubdrg  20753  lss1d  20954  lmhmeql  21046  lspextmo  21047  lspsnat  21139  lsppratlem6  21146  islbs3  21149  lbsextlem4  21155  lidl1el  21220  cnsubrg  21403  gsumfsum  21410  prmirredlem  21448  znidomb  21537  frgpcyg  21549  cssmre  21669  dsmmsubg  21719  dsmmlss  21720  frlmsslsp  21772  lindff1  21796  lindfrn  21797  rnasclassa  21871  mvrf1  21961  mplsubglem  21974  mpllsslem  21975  mplcoe1  22014  mplcoe5  22017  gsummoncoe1  22295  mat1dimcrng  22461  mdetdiaglem  22582  mdetunilem7  22602  mdetunilem8  22603  mdetunilem9  22604  cpmatacl  22700  cpmatmcllem  22702  mp2pm2mplem4  22793  en2top  22969  toponmre  23077  topssnei  23108  innei  23109  clslp  23132  restcls  23165  restntr  23166  ordtrest2lem  23187  cnpco  23251  cncls2  23257  cncnpi  23262  cncnp  23264  cnconst2  23267  cnpdis  23277  lmcnp  23288  cnhaus  23338  isreg2  23361  cncmp  23376  tgcmp  23385  sscmp  23389  cmpfi  23392  cnconn  23406  iunconnlem  23411  clsconn  23414  1stcfb  23429  1stcrest  23437  2ndcctbss  23439  2ndcdisj  23440  1stcelcls  23445  1stccnp  23446  restnlly  23466  cldllycmp  23479  lly1stc  23480  dislly  23481  locfincmp  23510  comppfsc  23516  kgentopon  23522  kgenidm  23531  1stckgenlem  23537  kgencn3  23542  ptpjpre1  23555  ptbasin  23561  txcls  23588  tx2cn  23594  ptpjcn  23595  ptclsg  23599  ptcnp  23606  txdis  23616  txlly  23620  txnlly  23621  pthaus  23622  txtube  23624  txcmplem1  23625  txcmplem2  23626  txcmp  23627  txhaus  23631  txkgen  23636  xkohaus  23637  xkococnlem  23643  xkococn  23644  txconn  23673  qtopeu  23700  qtoprest  23701  regr1lem2  23724  kqreglem1  23725  cmphaushmeo  23784  xkocnv  23798  fgabs  23863  filuni  23869  trufil  23894  ufileu  23903  filufint  23904  fin1aufil  23916  elfm2  23932  rnelfmlem  23936  fmfnfmlem2  23939  fmfnfmlem4  23941  fmufil  23943  flimopn  23959  fbflim2  23961  hausflimi  23964  hausflim  23965  flimcf  23966  flimclslem  23968  flimsncls  23970  hauspwpwf1  23971  cnpflfi  23983  fclsnei  24003  fclscf  24009  flimfnfcls  24012  fclscmp  24014  ufilcmp  24016  fcfnei  24019  cnpfcf  24025  alexsublem  24028  alexsub  24029  alexsubALTlem2  24032  alexsubALTlem3  24033  alexsubALTlem4  24034  ptcmplem3  24038  ptcmplem4  24039  ptcmplem5  24040  symgtgp  24090  tgpconncompeqg  24096  tgpconncomp  24097  ghmcnp  24099  tgpt0  24103  qustgplem  24105  haustsms2  24121  tsmsgsum  24123  tsmsres  24128  tsmsxp  24139  imasdsf1olem  24357  xbln0  24398  blssps  24408  blss  24409  neibl  24485  blcld  24489  metss  24492  metequiv2  24494  met1stc  24505  metrest  24508  prdsxmslem2  24513  metcnp3  24524  nrmmetd  24558  nlmvscnlem1  24670  nrginvrcnlem  24675  nmoleub  24715  icccmplem2  24808  icccmp  24810  reconnlem2  24812  xrge0tsms  24819  metdstri  24836  metdseq0  24839  metdscn  24841  cnmpopc  24914  lebnumlem3  24949  pcoval2  25002  pcopt  25008  nmoleub2lem  25100  nmhmcn  25106  ipcnlem1  25231  cfilfcls  25260  cmetcaulem  25274  iscmet3lem2  25278  iscmet3  25279  equivcau  25286  caubl  25294  bcthlem2  25311  bcthlem3  25312  bcthlem4  25313  bcthlem5  25314  ivthlem2  25438  ivthlem3  25439  ovoliunlem2  25489  ovolicc2lem2  25504  ovolicc2lem5  25507  ovolicc2  25508  ismbl2  25513  nulmbl  25521  nulmbl2  25522  unmbl  25523  shftmbl  25524  voliunlem3  25538  volsup  25542  ioombl1lem4  25547  ioombl1  25548  icombl  25550  ioombl  25551  uniioombl  25575  opnmbllem  25587  volivth  25593  vitali  25599  mbflimsup  25652  i1fadd  25681  itg1addlem4  25685  itg2le  25725  itg2seq  25728  itg2lea  25730  itg2splitlem  25734  itg2split  25735  itg2mono  25739  itg2gt0  25746  itg2cnlem2  25748  itgss  25798  itgfsum  25813  itgcn  25831  ellimc3  25865  limcco  25879  limciun  25880  dvnres  25917  dvnfre  25938  rolle  25976  c1liplem1  25982  dvivth  25996  dvne0  25997  lhop1lem  25999  lhop1  26000  lhop  26002  dvcnvrelem1  26003  dvfsumrlim  26017  dvfsum2  26020  ftc1a  26023  ftc1lem6  26027  itgsubst  26035  tdeglem4  26044  mdegaddle  26058  mdegvscale  26059  mdegmullem  26062  deg1tmle  26102  ply1divex  26121  dvdsq1p  26147  fta1g  26154  fta1b  26156  plyco0  26176  coeeulem  26208  dgrlem  26213  plyco  26225  coemullem  26234  dgreq0  26249  dgrco  26259  plydivex  26282  quotcan  26294  aannenlem1  26313  aalioulem2  26318  aalioulem3  26319  taylthlem1  26357  ulmbdd  26382  itgulm  26392  radcnvlt1  26402  psercnlem1  26409  abelthlem2  26416  abelthlem8  26423  logcnlem5  26629  efopn  26641  cxpmul2z  26674  cxpcn3lem  26730  cxpeq  26740  xrlimcnp  26951  cxplim  26954  o1cxp  26957  cxploglim  26960  scvxcvx  26968  jensen  26971  ftalem1  27055  ftalem2  27056  fta  27062  basellem3  27065  isppw2  27097  ppinprm  27134  chtnprm  27136  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chtublem  27193  perfectlem2  27212  dchrfi  27237  dchrptlem1  27246  dchrptlem2  27247  dchrptlem3  27248  dchrsum2  27250  bposlem1  27266  bposlem3  27268  2sqlem5  27404  2sqlem6  27405  2sqlem8  27408  2sqlem10  27410  2sqb  27414  chebbnd1lem1  27451  chtppilimlem2  27456  dchrisum0flb  27492  dchrisum0fno1  27493  dchrisum0  27502  pntrsumbnd2  27549  pntpbnd1  27568  pntpbnd2  27569  pntlemp  27592  pnt3  27594  qabvle  27607  ostth2lem2  27616  ostth3  27620  ostth  27621  nolt02o  27678  nogt01o  27679  nosupprefixmo  27683  noinfprefixmo  27684  nosupbnd1lem3  27693  nosupbnd1lem4  27694  nosupbnd1lem5  27695  noinfbnd1lem3  27708  noinfbnd1lem4  27709  noinfbnd1lem5  27710  noetasuplem4  27719  noetainflem4  27723  etaslts  27804  cuteq1  27828  madebdaylemlrcut  27910  cutlt  27943  mulsuniflem  28160  bdayons  28287  addonbday  28290  om2noseqlt  28310  n0fincut  28366  bdaypw2n0bndlem  28474  bdayfinbndlem1  28478  z12sge0  28494  readdscl  28510  remulscl  28513  colinearalglem4  28997  axcontlem10  29061  upgrex  29180  smcnlem  30787  ubthlem1  30960  ubthlem3  30962  htthlem  31007  5oalem6  31749  leopmuli  32223  pjnormssi  32258  pjclem4  32289  pj3si  32297  hatomistici  32452  sumdmdlem  32508  sgn3da  32927  wrdt2ind  33033  xrge0tsmsd  33155  isarchiofld  33281  ordtrest2NEWlem  34115  qqhf  34179  eulerpartlemb  34561  ballotlemfc0  34686  ballotlemfcc  34687  subfacp1lem5  35421  erdszelem7  35434  erdszelem11  35438  pconnconn  35468  txpconn  35469  connpconn  35472  sconnpi1  35476  txsconn  35478  cvxsconn  35480  cvmopnlem  35515  cvmfolem  35516  cvmliftmolem2  35519  cvmliftlem7  35528  cvmliftlem10  35531  cvmlift2lem10  35549  cvmlift3lem4  35559  cvmlift3lem8  35563  satfun  35648  msubff1  35793  wzel  36059  wsuclem  36060  btwnouttr2  36259  cgrxfr  36292  btwnxfr  36293  brcolinear  36296  lineext  36313  btwnconn1lem13  36336  midofsegid  36341  segcon2  36342  brsegle  36345  seglecgr12im  36347  segletr  36351  colinbtwnle  36355  broutsideof2  36359  btwnoutside  36362  broutsideof3  36363  outsideoftr  36366  outsideofeq  36367  outsideofeu  36368  outsidele  36369  lineunray  36384  lineelsb2  36385  linethru  36390  finminlem  36555  nn0prpwlem  36559  neibastop2lem  36597  neibastop2  36598  neibastop3  36599  topjoin  36602  tailfb  36614  axtcond  36715  relowlssretop  37734  fvineqsneq  37783  wl-sbcom2d-lem1  37939  finixpnum  37981  poimirlem6  38002  poimirlem7  38003  poimirlem13  38009  poimirlem26  38022  poimirlem29  38025  heicant  38031  opnmbllem0  38032  mblfinlem3  38035  ismblfin  38037  ovoliunnfl  38038  voliunnfl  38040  volsupnfl  38041  itg2addnclem  38047  itg2addnclem3  38049  ftc1cnnc  38068  sdclem2  38118  fdc  38121  istotbnd3  38147  isbnd2  38159  isbnd3  38160  prdsbnd  38169  cntotbnd  38172  heibor1lem  38185  heibor1  38186  heiborlem10  38196  rrncmslem  38208  ghomco  38267  1idl  38402  unichnidl  38407  disjlem18  39279  prtlem10  39366  prtlem18  39378  atlatmstc  39820  cvrexchlem  39920  paddasslem14  40334  pexmidlem5N  40475  cdleme29ex  40875  cdlemefr29exN  40903  cdleme32fva  40938  diarnN  41630  dihlsscpre  41735  isnacs3  43168  fnwe2lem2  43505  kelac1  43517  hbtlem5  43582  hbt  43584  dgraa0p  43603  ofoafg  43808  ofoafo  43810  naddcnffo  43818  fzunt  43908  fzuntd  43909  monoordxrv  45932  rlimdmafv  47648  rlimdmafv2  47729  fmtnoprmfac2  48053  perfectALTVlem2  48221  mogoldbb  48284  lindslinindsimp2  48962