Theorem expr 459

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  animpimp2impd  842  3expia  1117  reximddv  3275  rexlimdvaa  3285  disjxiun  5063  wereu2  5552  ordtr3  6236  fcof1  7043  knatar  7110  riota5f  7142  ovmpodf  7306  extmptsuppeq  7854  suppss  7860  suppss2  7864  wfrlem17  7971  smoord  8002  tfrlem9a  8022  oaass  8187  oelimcl  8226  oaabs2  8272  swoso  8322  eceqoveq  8402  domdifsn  8600  domunsncan  8617  omxpenlem  8618  enfixsn  8626  mapdom2  8688  frfi  8763  fofinf1o  8799  finsschain  8831  elfiun  8894  marypha1lem  8897  eqsupd  8921  eqinfd  8949  ordiso2  8979  ordtypelem6  8987  ordtypelem7  8988  ordtypelem10  8991  oismo  9004  wemapsolem  9014  brwdom2  9037  wdomtr  9039  unwdomg  9048  xpwdomg  9049  unxpwdom2  9052  cantnfval2  9132  cantnfle  9134  cantnflem1  9152  cantnf  9156  r1ordg  9207  tcrank  9313  carddomi2  9399  harval2  9426  infxpenlem  9439  infxpenc2lem2  9446  fseqenlem1  9450  dfac8clem  9458  acndom2  9480  infpwfien  9488  iunfictbso  9540  dfac12lem3  9571  infxp  9637  coflim  9683  cofsmo  9691  coftr  9695  sornom  9699  infpssrlem4  9728  enfin2i  9743  fin23lem26  9747  fin23lem27  9750  fin23lem36  9770  fin23lem40  9773  isf32lem5  9779  isf34lem4  9799  isfin1-3  9808  fin1a2lem10  9831  fin1a2lem13  9834  fin1a2s  9836  hsmexlem4  9851  ttukeylem5  9935  ttukeylem6  9936  ttukeylem7  9937  alephval2  9994  gchor  10049  fpwwe2lem7  10058  fpwwe2lem12  10063  fpwwe2  10065  pwfseqlem4a  10083  pwfseqlem4  10084  winalim2  10118  gchina  10121  inar1  10197  nqereq  10357  prlem934  10455  prlem936  10469  addsrmo  10495  mulsrmo  10496  supsrlem  10533  axpre-sup  10591  dedekind  10803  dedekindle  10804  mulge0b  11510  supaddc  11608  supmul1  11610  un0addcl  11931  un0mulcl  11932  uzwo3  12344  qbtwnre  12593  xlemul1a  12682  seqcl2  13389  seqfveq2  13393  seqshft2  13397  monoord  13401  seqsplit  13404  seqf1olem1  13410  seqid2  13417  seqhomo  13418  expnegz  13464  expcan  13534  ltexp2  13535  discr  13602  bcval5  13679  hashbc  13812  hashf1lem2  13815  seqcoll  13823  seqcoll2  13824  wrdind  14084  wrd2ind  14085  cau3lem  14714  ello1d  14880  lo1bdd2  14881  rlimclim  14903  climrlim2  14904  rlimdm  14908  rlimcn1  14945  reccn2  14953  rlimsqzlem  15005  lo1le  15008  caucvgrlem  15029  caurcvg2  15034  summolem2  15073  zsum  15075  fsum  15077  fsumf1o  15080  sumss  15081  fsumss  15082  fsumcl2lem  15088  fsumadd  15096  fsumcom2  15129  fsum0diag2  15138  fsummulc2  15139  fsumconst  15145  fsumrelem  15162  fsumrlim  15166  fsumo1  15167  divrcnv  15207  geomulcvg  15232  mertenslem2  15241  prodmolem2  15289  zprod  15291  fprod  15295  fprodf1o  15300  prodss  15301  fprodss  15302  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodconst  15332  fprodn0  15333  fprodcom2  15338  ruclem8  15590  dvds0lem  15620  dvdsnegb  15627  dvdssub2  15651  bitsf1  15795  bitsshft  15824  bezoutlem3  15889  bezoutlem4  15890  isprm5  16051  isprm6  16058  hashgcdeq  16126  modprminv  16136  modprminveq  16137  reumodprminv  16141  pcqmul  16190  pcqcl  16193  pcxcl  16197  pc2dvds  16215  pcadd  16225  pcmpt  16228  pockthg  16242  infpnlem1  16246  prmreclem5  16256  vdwlem2  16318  vdwlem9  16325  vdwlem10  16326  vdwlem12  16328  ramub  16349  0ram  16356  ramub1lem2  16363  ramub1  16364  ramcl  16365  mreexexd  16919  acsfn2  16934  iscatd  16944  catpropd  16979  setcmon  17347  pleval2i  17574  psss  17824  mgmidsssn0  17882  mhmeql  17990  frmdss2  18028  frmdup3  18032  grprcan  18137  dfgrp3lem  18197  mulgnn0ass  18263  isnsg3  18312  ghmpreima  18380  ghmeql  18381  gaorber  18438  f1omvdco2  18576  psgnunilem1  18621  psgnunilem2  18623  oddvds  18675  gexdvds  18709  sylow1lem1  18723  odcau  18729  pgpssslw  18739  sylow2alem2  18743  sylow2blem3  18747  fislw  18750  lsmmod  18801  efgredlem  18873  frgpup3  18904  gsumval3  19027  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  gsum2d2lem  19093  ablfac1eulem  19194  pgpfac1lem5  19201  ablfaclem3  19209  issubdrg  19560  lss1d  19735  lmhmeql  19827  lspextmo  19828  lspsnat  19917  lsppratlem6  19924  islbs3  19927  lbsextlem4  19933  lidl1el  19991  rnasclassa  20124  mvrf1  20205  mplsubglem  20214  mpllsslem  20215  mplcoe1  20246  mplcoe5  20249  gsummoncoe1  20472  cnsubrg  20605  gsumfsum  20612  prmirredlem  20640  znidomb  20708  frgpcyg  20720  cssmre  20837  dsmmsubg  20887  dsmmlss  20888  frlmsslsp  20940  lindff1  20964  lindfrn  20965  mat1dimcrng  21086  mdetdiaglem  21207  mdetunilem7  21227  mdetunilem8  21228  mdetunilem9  21229  cpmatacl  21324  cpmatmcllem  21326  mp2pm2mplem4  21417  en2top  21593  toponmre  21701  topssnei  21732  innei  21733  clslp  21756  restcls  21789  restntr  21790  ordtrest2lem  21811  cnpco  21875  cncls2  21881  cncnpi  21886  cncnp  21888  cnconst2  21891  cnpdis  21901  lmcnp  21912  cnhaus  21962  isreg2  21985  cncmp  22000  tgcmp  22009  sscmp  22013  cmpfi  22016  cnconn  22030  iunconnlem  22035  clsconn  22038  1stcfb  22053  1stcrest  22061  2ndcctbss  22063  2ndcdisj  22064  1stcelcls  22069  1stccnp  22070  restnlly  22090  cldllycmp  22103  lly1stc  22104  dislly  22105  locfincmp  22134  comppfsc  22140  kgentopon  22146  kgenidm  22155  1stckgenlem  22161  kgencn3  22166  ptpjpre1  22179  ptbasin  22185  txcls  22212  tx2cn  22218  ptpjcn  22219  ptclsg  22223  ptcnp  22230  txdis  22240  txlly  22244  txnlly  22245  pthaus  22246  txtube  22248  txcmplem1  22249  txcmplem2  22250  txcmp  22251  txhaus  22255  txkgen  22260  xkohaus  22261  xkococnlem  22267  xkococn  22268  txconn  22297  qtopeu  22324  qtoprest  22325  regr1lem2  22348  kqreglem1  22349  cmphaushmeo  22408  xkocnv  22422  fgabs  22487  filuni  22493  trufil  22518  ufileu  22527  filufint  22528  fin1aufil  22540  elfm2  22556  rnelfmlem  22560  fmfnfmlem2  22563  fmfnfmlem4  22565  fmufil  22567  flimopn  22583  fbflim2  22585  hausflimi  22588  hausflim  22589  flimcf  22590  flimclslem  22592  flimsncls  22594  hauspwpwf1  22595  cnpflfi  22607  fclsnei  22627  fclscf  22633  flimfnfcls  22636  fclscmp  22638  ufilcmp  22640  fcfnei  22643  cnpfcf  22649  alexsublem  22652  alexsub  22653  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem3  22662  ptcmplem4  22663  ptcmplem5  22664  symgtgp  22714  tgpconncompeqg  22720  tgpconncomp  22721  ghmcnp  22723  tgpt0  22727  qustgplem  22729  haustsms2  22745  tsmsgsum  22747  tsmsres  22752  tsmsxp  22763  imasdsf1olem  22983  xbln0  23024  blssps  23034  blss  23035  neibl  23111  blcld  23115  metss  23118  metequiv2  23120  met1stc  23131  metrest  23134  prdsxmslem2  23139  metcnp3  23150  nrmmetd  23184  nlmvscnlem1  23295  nrginvrcnlem  23300  nmoleub  23340  icccmplem2  23431  icccmp  23433  reconnlem2  23435  xrge0tsms  23442  metdstri  23459  metdseq0  23462  metdscn  23464  cnmpopc  23532  lebnumlem3  23567  pcoval2  23620  pcopt  23626  nmoleub2lem  23718  nmhmcn  23724  ipcnlem1  23848  cfilfcls  23877  cmetcaulem  23891  iscmet3lem2  23895  iscmet3  23896  equivcau  23903  caubl  23911  bcthlem2  23928  bcthlem3  23929  bcthlem4  23930  bcthlem5  23931  ivthlem2  24053  ivthlem3  24054  ovoliunlem2  24104  ovolicc2lem2  24119  ovolicc2lem5  24122  ovolicc2  24123  ismbl2  24128  nulmbl  24136  nulmbl2  24137  unmbl  24138  shftmbl  24139  voliunlem3  24153  volsup  24157  ioombl1lem4  24162  ioombl1  24163  icombl  24165  ioombl  24166  uniioombl  24190  opnmbllem  24202  volivth  24208  vitali  24214  mbflimsup  24267  i1fadd  24296  itg1addlem4  24300  itg2le  24340  itg2seq  24343  itg2lea  24345  itg2splitlem  24349  itg2split  24350  itg2mono  24354  itg2gt0  24361  itg2cnlem2  24363  itgss  24412  itgfsum  24427  itgcn  24443  ellimc3  24477  limcco  24491  limciun  24492  dvnres  24528  dvnfre  24549  rolle  24587  c1liplem1  24593  dvivth  24607  dvne0  24608  lhop1lem  24610  lhop1  24611  lhop  24613  dvcnvrelem1  24614  dvfsumrlim  24628  dvfsum2  24631  ftc1a  24634  ftc1lem6  24638  itgsubst  24646  tdeglem4  24654  mdegaddle  24668  mdegvscale  24669  mdegmullem  24672  deg1tmle  24711  ply1divex  24730  dvdsq1p  24754  fta1g  24761  fta1b  24763  plyco0  24782  coeeulem  24814  dgrlem  24819  plyco  24831  coemullem  24840  dgreq0  24855  dgrco  24865  plydivex  24886  quotcan  24898  aannenlem1  24917  aalioulem2  24922  aalioulem3  24923  taylthlem1  24961  ulmbdd  24986  itgulm  24996  radcnvlt1  25006  psercnlem1  25013  abelthlem2  25020  abelthlem8  25027  logcnlem5  25229  efopn  25241  cxpmul2z  25274  cxpcn3lem  25328  cxpeq  25338  xrlimcnp  25546  cxplim  25549  o1cxp  25552  cxploglim  25555  scvxcvx  25563  jensen  25566  ftalem1  25650  ftalem2  25651  fta  25657  basellem3  25660  isppw2  25692  ppinprm  25729  chtnprm  25731  dvdsmulf1o  25771  chtublem  25787  perfectlem2  25806  dchrfi  25831  dchrptlem1  25840  dchrptlem2  25841  dchrptlem3  25842  dchrsum2  25844  bposlem1  25860  bposlem3  25862  2sqlem5  25998  2sqlem6  25999  2sqlem8  26002  2sqlem10  26004  2sqb  26008  chebbnd1lem1  26045  chtppilimlem2  26050  dchrisum0flb  26086  dchrisum0fno1  26087  dchrisum0  26096  pntrsumbnd2  26143  pntpbnd1  26162  pntpbnd2  26163  pntlemp  26186  pnt3  26188  qabvle  26201  ostth2lem2  26210  ostth3  26214  ostth  26215  colinearalglem4  26695  axcontlem10  26759  upgrex  26877  smcnlem  28474  ubthlem1  28647  ubthlem3  28649  htthlem  28694  5oalem6  29436  leopmuli  29910  pjnormssi  29945  pjclem4  29976  pj3si  29984  hatomistici  30139  sumdmdlem  30195  wrdt2ind  30627  xrge0tsmsd  30692  isarchiofld  30890  ordtrest2NEWlem  31165  qqhf  31227  eulerpartlemb  31626  ballotlemfc0  31750  ballotlemfcc  31751  sgn3da  31799  subfacp1lem5  32431  erdszelem7  32444  erdszelem11  32448  pconnconn  32478  txpconn  32479  connpconn  32482  sconnpi1  32486  txsconn  32488  cvxsconn  32490  cvmopnlem  32525  cvmfolem  32526  cvmliftmolem2  32529  cvmliftlem7  32538  cvmliftlem10  32541  cvmlift2lem10  32559  cvmlift3lem4  32569  cvmlift3lem8  32573  satfun  32658  msubff1  32803  frpomin  33078  wzel  33111  wsuclem  33112  frrlem14  33136  nolt02o  33199  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  noetalem3  33219  btwnouttr2  33483  cgrxfr  33516  btwnxfr  33517  brcolinear  33520  lineext  33537  btwnconn1lem13  33560  midofsegid  33565  segcon2  33566  brsegle  33569  seglecgr12im  33571  segletr  33575  colinbtwnle  33579  broutsideof2  33583  btwnoutside  33586  broutsideof3  33587  outsideoftr  33590  outsideofeq  33591  outsideofeu  33592  outsidele  33593  lineunray  33608  lineelsb2  33609  linethru  33614  finminlem  33666  nn0prpwlem  33670  neibastop2lem  33708  neibastop2  33709  neibastop3  33710  topjoin  33713  tailfb  33725  relowlssretop  34647  fvineqsneq  34696  wl-sbcom2d-lem1  34810  finixpnum  34892  poimirlem6  34913  poimirlem7  34914  poimirlem13  34920  poimirlem26  34933  poimirlem29  34936  heicant  34942  opnmbllem0  34943  mblfinlem3  34946  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  itg2addnclem3  34960  ftc1cnnc  34981  sdclem2  35032  fdc  35035  istotbnd3  35064  isbnd2  35076  isbnd3  35077  prdsbnd  35086  cntotbnd  35089  heibor1lem  35102  heibor1  35103  heiborlem10  35113  rrncmslem  35125  ghomco  35184  1idl  35319  unichnidl  35324  prtlem10  36016  prtlem18  36028  atlatmstc  36470  cvrexchlem  36570  paddasslem14  36984  pexmidlem5N  37125  cdleme29ex  37525  cdlemefr29exN  37553  cdleme32fva  37588  diarnN  38280  dihlsscpre  38385  isnacs3  39356  fnwe2lem2  39700  kelac1  39712  hbtlem5  39777  hbt  39779  dgraa0p  39798  monoordxrv  41807  rlimdmafv  43425  rlimdmafv2  43506  fmtnoprmfac2  43778  perfectALTVlem2  43936  mogoldbb  43999  mgmhmeql  44119  lindslinindsimp2  44567