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

This theorem is referenced by:  animpimp2impd  846  3expia  1121  rexlimdvaa  3136  reximddv  3150  disjxiun  5093  wereu2  5619  frpomin  6296  ordtr3  6361  fcof1  7231  knatar  7301  riota5f  7341  ovmpodf  7512  extmptsuppeq  8128  suppss  8134  suppss2  8140  frrlem14  8239  fprresex  8250  smoord  8295  tfrlem9a  8315  oaass  8486  oelimcl  8526  oaabs2  8575  cofon1  8598  naddssim  8611  swoso  8667  eceqoveq  8757  domdifsn  8986  domunsncan  9003  omxpenlem  9004  enfixsn  9012  mapdom2  9074  frfi  9183  fofinf1o  9230  finsschain  9257  elfiun  9331  marypha1lem  9334  eqsupd  9358  eqinfd  9387  ordiso2  9418  ordtypelem6  9426  ordtypelem7  9427  ordtypelem10  9430  oismo  9443  wemapsolem  9453  brwdom2  9476  wdomtr  9478  unwdomg  9487  xpwdomg  9488  unxpwdom2  9491  cantnfval2  9576  cantnfle  9578  cantnflem1  9596  cantnf  9600  r1ordg  9688  tcrank  9794  carddomi2  9880  harval2  9907  infxpenlem  9921  infxpenc2lem2  9928  fseqenlem1  9932  dfac8clem  9940  acndom2  9962  infpwfien  9970  iunfictbso  10022  dfac12lem3  10054  infxp  10122  coflim  10169  cofsmo  10177  coftr  10181  sornom  10185  infpssrlem4  10214  enfin2i  10229  fin23lem26  10233  fin23lem27  10236  fin23lem36  10256  fin23lem40  10259  isf32lem5  10265  isf34lem4  10285  isfin1-3  10294  fin1a2lem10  10317  fin1a2lem13  10320  fin1a2s  10322  hsmexlem4  10337  ttukeylem5  10421  ttukeylem6  10422  ttukeylem7  10423  alephval2  10481  gchor  10536  fpwwe2lem6  10545  fpwwe2lem11  10550  fpwwe2  10552  pwfseqlem4a  10570  pwfseqlem4  10571  winalim2  10605  gchina  10608  inar1  10684  nqereq  10844  prlem934  10942  prlem936  10956  addsrmo  10982  mulsrmo  10983  supsrlem  11020  axpre-sup  11078  dedekind  11294  dedekindle  11295  mulge0b  12010  supaddc  12107  supmul1  12109  un0addcl  12432  un0mulcl  12433  uzwo3  12854  qbtwnre  13112  xlemul1a  13201  seqcl2  13941  seqfveq2  13945  seqshft2  13949  monoord  13953  seqsplit  13956  seqf1olem1  13962  seqid2  13969  seqhomo  13970  expnegz  14017  expcan  14090  ltexp2  14091  discr  14161  bcval5  14239  hashbc  14374  hashf1lem2  14377  seqcoll  14385  seqcoll2  14386  wrdind  14643  wrd2ind  14644  cau3lem  15276  ello1d  15444  lo1bdd2  15445  rlimclim  15467  climrlim2  15468  rlimdm  15472  rlimcn1  15509  reccn2  15518  rlimsqzlem  15570  lo1le  15573  caucvgrlem  15594  caurcvg2  15599  summolem2  15637  zsum  15639  fsum  15641  fsumf1o  15644  sumss  15645  fsumss  15646  fsumcl2lem  15652  fsumadd  15661  fsumcom2  15695  fsum0diag2  15704  fsummulc2  15705  fsumconst  15711  fsumrelem  15728  fsumrlim  15732  fsumo1  15733  divrcnv  15773  geomulcvg  15797  mertenslem2  15806  prodmolem2  15856  zprod  15858  fprod  15862  fprodf1o  15867  prodss  15868  fprodss  15869  fprodcl2lem  15871  fprodmul  15881  fproddiv  15882  fprodconst  15899  fprodn0  15900  fprodcom2  15905  ruclem8  16160  dvds0lem  16191  dvdsnegb  16198  dvdssub2  16226  bitsf1  16371  bitsshft  16400  bezoutlem3  16466  bezoutlem4  16467  isprm5  16632  isprm6  16639  hashgcdeq  16715  modprminv  16725  modprminveq  16726  reumodprminv  16730  pcqmul  16779  pcqcl  16782  pcxnn0cl  16786  pcxcl  16787  pc2dvds  16805  pcadd  16815  pcmpt  16818  pockthg  16832  infpnlem1  16836  prmreclem5  16846  vdwlem2  16908  vdwlem9  16915  vdwlem10  16916  vdwlem12  16918  ramub  16939  0ram  16946  ramub1lem2  16953  ramub1  16954  ramcl  16955  mreexexd  17569  acsfn2  17584  iscatd  17594  catpropd  17630  setcmon  18009  pleval2i  18255  psss  18501  mgmidsssn0  18595  mgmhmeql  18639  mhmeql  18749  frmdss2  18786  frmdup3  18790  grprcan  18901  dfgrp3lem  18966  mulgnn0ass  19038  isnsg3  19087  ghmpreima  19165  ghmeql  19166  gaorber  19235  f1omvdco2  19375  psgnunilem1  19420  psgnunilem2  19422  oddvds  19474  gexdvds  19511  sylow1lem1  19525  odcau  19531  pgpssslw  19541  sylow2alem2  19545  sylow2blem3  19549  fislw  19552  lsmmod  19602  efgredlem  19674  frgpup3  19705  gsumval3  19834  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  gsum2d2lem  19900  ablfac1eulem  20001  pgpfac1lem5  20008  ablfaclem3  20016  issubdrg  20711  lss1d  20912  lmhmeql  21005  lspextmo  21006  lspsnat  21098  lsppratlem6  21105  islbs3  21108  lbsextlem4  21114  lidl1el  21179  cnsubrg  21380  gsumfsum  21387  prmirredlem  21425  znidomb  21514  frgpcyg  21526  cssmre  21646  dsmmsubg  21696  dsmmlss  21697  frlmsslsp  21749  lindff1  21773  lindfrn  21774  rnasclassa  21849  mvrf1  21939  mplsubglem  21952  mpllsslem  21953  mplcoe1  21990  mplcoe5  21993  gsummoncoe1  22250  mat1dimcrng  22419  mdetdiaglem  22540  mdetunilem7  22560  mdetunilem8  22561  mdetunilem9  22562  cpmatacl  22658  cpmatmcllem  22660  mp2pm2mplem4  22751  en2top  22927  toponmre  23035  topssnei  23066  innei  23067  clslp  23090  restcls  23123  restntr  23124  ordtrest2lem  23145  cnpco  23209  cncls2  23215  cncnpi  23220  cncnp  23222  cnconst2  23225  cnpdis  23235  lmcnp  23246  cnhaus  23296  isreg2  23319  cncmp  23334  tgcmp  23343  sscmp  23347  cmpfi  23350  cnconn  23364  iunconnlem  23369  clsconn  23372  1stcfb  23387  1stcrest  23395  2ndcctbss  23397  2ndcdisj  23398  1stcelcls  23403  1stccnp  23404  restnlly  23424  cldllycmp  23437  lly1stc  23438  dislly  23439  locfincmp  23468  comppfsc  23474  kgentopon  23480  kgenidm  23489  1stckgenlem  23495  kgencn3  23500  ptpjpre1  23513  ptbasin  23519  txcls  23546  tx2cn  23552  ptpjcn  23553  ptclsg  23557  ptcnp  23564  txdis  23574  txlly  23578  txnlly  23579  pthaus  23580  txtube  23582  txcmplem1  23583  txcmplem2  23584  txcmp  23585  txhaus  23589  txkgen  23594  xkohaus  23595  xkococnlem  23601  xkococn  23602  txconn  23631  qtopeu  23658  qtoprest  23659  regr1lem2  23682  kqreglem1  23683  cmphaushmeo  23742  xkocnv  23756  fgabs  23821  filuni  23827  trufil  23852  ufileu  23861  filufint  23862  fin1aufil  23874  elfm2  23890  rnelfmlem  23894  fmfnfmlem2  23897  fmfnfmlem4  23899  fmufil  23901  flimopn  23917  fbflim2  23919  hausflimi  23922  hausflim  23923  flimcf  23924  flimclslem  23926  flimsncls  23928  hauspwpwf1  23929  cnpflfi  23941  fclsnei  23961  fclscf  23967  flimfnfcls  23970  fclscmp  23972  ufilcmp  23974  fcfnei  23977  cnpfcf  23983  alexsublem  23986  alexsub  23987  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  ptcmplem3  23996  ptcmplem4  23997  ptcmplem5  23998  symgtgp  24048  tgpconncompeqg  24054  tgpconncomp  24055  ghmcnp  24057  tgpt0  24061  qustgplem  24063  haustsms2  24079  tsmsgsum  24081  tsmsres  24086  tsmsxp  24097  imasdsf1olem  24315  xbln0  24356  blssps  24366  blss  24367  neibl  24443  blcld  24447  metss  24450  metequiv2  24452  met1stc  24463  metrest  24466  prdsxmslem2  24471  metcnp3  24482  nrmmetd  24516  nlmvscnlem1  24628  nrginvrcnlem  24633  nmoleub  24673  icccmplem2  24766  icccmp  24768  reconnlem2  24770  xrge0tsms  24777  metdstri  24794  metdseq0  24797  metdscn  24799  cnmpopc  24876  lebnumlem3  24916  pcoval2  24970  pcopt  24976  nmoleub2lem  25068  nmhmcn  25074  ipcnlem1  25199  cfilfcls  25228  cmetcaulem  25242  iscmet3lem2  25246  iscmet3  25247  equivcau  25254  caubl  25262  bcthlem2  25279  bcthlem3  25280  bcthlem4  25281  bcthlem5  25282  ivthlem2  25407  ivthlem3  25408  ovoliunlem2  25458  ovolicc2lem2  25473  ovolicc2lem5  25476  ovolicc2  25477  ismbl2  25482  nulmbl  25490  nulmbl2  25491  unmbl  25492  shftmbl  25493  voliunlem3  25507  volsup  25511  ioombl1lem4  25516  ioombl1  25517  icombl  25519  ioombl  25520  uniioombl  25544  opnmbllem  25556  volivth  25562  vitali  25568  mbflimsup  25621  i1fadd  25650  itg1addlem4  25654  itg2le  25694  itg2seq  25697  itg2lea  25699  itg2splitlem  25703  itg2split  25704  itg2mono  25708  itg2gt0  25715  itg2cnlem2  25717  itgss  25767  itgfsum  25782  itgcn  25800  ellimc3  25834  limcco  25848  limciun  25849  dvnres  25887  dvnfre  25910  rolle  25948  c1liplem1  25955  dvivth  25969  dvne0  25970  lhop1lem  25972  lhop1  25973  lhop  25975  dvcnvrelem1  25976  dvfsumrlim  25992  dvfsum2  25995  ftc1a  25998  ftc1lem6  26002  itgsubst  26010  tdeglem4  26019  mdegaddle  26033  mdegvscale  26034  mdegmullem  26037  deg1tmle  26077  ply1divex  26096  dvdsq1p  26122  fta1g  26129  fta1b  26131  plyco0  26151  coeeulem  26183  dgrlem  26188  plyco  26200  coemullem  26209  dgreq0  26225  dgrco  26235  plydivex  26259  quotcan  26271  aannenlem1  26290  aalioulem2  26295  aalioulem3  26296  taylthlem1  26335  ulmbdd  26361  itgulm  26371  radcnvlt1  26381  psercnlem1  26389  abelthlem2  26396  abelthlem8  26403  logcnlem5  26609  efopn  26621  cxpmul2z  26654  cxpcn3lem  26711  cxpeq  26721  xrlimcnp  26932  cxplim  26936  o1cxp  26939  cxploglim  26942  scvxcvx  26950  jensen  26953  ftalem1  27037  ftalem2  27038  fta  27044  basellem3  27047  isppw2  27079  ppinprm  27116  chtnprm  27118  mpodvdsmulf1o  27158  dvdsmulf1o  27160  chtublem  27176  perfectlem2  27195  dchrfi  27220  dchrptlem1  27229  dchrptlem2  27230  dchrptlem3  27231  dchrsum2  27233  bposlem1  27249  bposlem3  27251  2sqlem5  27387  2sqlem6  27388  2sqlem8  27391  2sqlem10  27393  2sqb  27397  chebbnd1lem1  27434  chtppilimlem2  27439  dchrisum0flb  27475  dchrisum0fno1  27476  dchrisum0  27485  pntrsumbnd2  27532  pntpbnd1  27551  pntpbnd2  27552  pntlemp  27575  pnt3  27577  qabvle  27590  ostth2lem2  27599  ostth3  27603  ostth  27604  nolt02o  27661  nogt01o  27662  nosupprefixmo  27666  noinfprefixmo  27667  nosupbnd1lem3  27676  nosupbnd1lem4  27677  nosupbnd1lem5  27678  noinfbnd1lem3  27691  noinfbnd1lem4  27692  noinfbnd1lem5  27693  noetasuplem4  27702  noetainflem4  27706  etasslt  27781  cuteq1  27805  madebdaylemlrcut  27871  cutlt  27903  mulsuniflem  28118  bdayon  28240  om2noseqlt  28260  n0sfincut  28315  bdaypw2n0s  28420  zs12ge0  28432  readdscl  28444  remulscl  28447  colinearalglem4  28931  axcontlem10  28995  upgrex  29114  smcnlem  30721  ubthlem1  30894  ubthlem3  30896  htthlem  30941  5oalem6  31683  leopmuli  32157  pjnormssi  32192  pjclem4  32223  pj3si  32231  hatomistici  32386  sumdmdlem  32442  sgn3da  32864  wrdt2ind  32984  xrge0tsmsd  33104  isarchiofld  33230  ordtrest2NEWlem  34028  qqhf  34092  eulerpartlemb  34474  ballotlemfc0  34599  ballotlemfcc  34600  subfacp1lem5  35327  erdszelem7  35340  erdszelem11  35344  pconnconn  35374  txpconn  35375  connpconn  35378  sconnpi1  35382  txsconn  35384  cvxsconn  35386  cvmopnlem  35421  cvmfolem  35422  cvmliftmolem2  35425  cvmliftlem7  35434  cvmliftlem10  35437  cvmlift2lem10  35455  cvmlift3lem4  35465  cvmlift3lem8  35469  satfun  35554  msubff1  35699  wzel  35965  wsuclem  35966  btwnouttr2  36165  cgrxfr  36198  btwnxfr  36199  brcolinear  36202  lineext  36219  btwnconn1lem13  36242  midofsegid  36247  segcon2  36248  brsegle  36251  seglecgr12im  36253  segletr  36257  colinbtwnle  36261  broutsideof2  36265  btwnoutside  36268  broutsideof3  36269  outsideoftr  36272  outsideofeq  36273  outsideofeu  36274  outsidele  36275  lineunray  36290  lineelsb2  36291  linethru  36296  finminlem  36461  nn0prpwlem  36465  neibastop2lem  36503  neibastop2  36504  neibastop3  36505  topjoin  36508  tailfb  36520  relowlssretop  37507  fvineqsneq  37556  wl-sbcom2d-lem1  37703  finixpnum  37745  poimirlem6  37766  poimirlem7  37767  poimirlem13  37773  poimirlem26  37786  poimirlem29  37789  heicant  37795  opnmbllem0  37796  mblfinlem3  37799  ismblfin  37801  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  itg2addnclem  37811  itg2addnclem3  37813  ftc1cnnc  37832  sdclem2  37882  fdc  37885  istotbnd3  37911  isbnd2  37923  isbnd3  37924  prdsbnd  37933  cntotbnd  37936  heibor1lem  37949  heibor1  37950  heiborlem10  37960  rrncmslem  37972  ghomco  38031  1idl  38166  unichnidl  38171  disjlem18  38998  prtlem10  39064  prtlem18  39076  atlatmstc  39518  cvrexchlem  39618  paddasslem14  40032  pexmidlem5N  40173  cdleme29ex  40573  cdlemefr29exN  40601  cdleme32fva  40636  diarnN  41328  dihlsscpre  41433  isnacs3  42894  fnwe2lem2  43235  kelac1  43247  hbtlem5  43312  hbt  43314  dgraa0p  43333  ofoafg  43538  ofoafo  43540  naddcnffo  43548  fzunt  43638  fzuntd  43639  monoordxrv  45667  rlimdmafv  47365  rlimdmafv2  47446  fmtnoprmfac2  47755  perfectALTVlem2  47910  mogoldbb  47973  lindslinindsimp2  48651