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  845  3expia  1121  rexlimdvaa  3158  reximddv  3173  disjxiun  5166  wereu2  5696  frpomin  6371  ordtr3  6439  fcof1  7321  knatar  7390  riota5f  7430  ovmpodf  7602  extmptsuppeq  8225  suppss  8231  suppss2  8237  frrlem14  8336  fprresex  8347  wfrlem17OLD  8377  smoord  8417  tfrlem9a  8438  oaass  8613  oelimcl  8652  oaabs2  8701  cofon1  8724  naddssim  8737  swoso  8793  eceqoveq  8876  domdifsn  9116  domunsncan  9134  omxpenlem  9135  enfixsn  9143  mapdom2  9210  frfi  9345  fofinf1o  9396  finsschain  9425  elfiun  9495  marypha1lem  9498  eqsupd  9522  eqinfd  9550  ordiso2  9580  ordtypelem6  9588  ordtypelem7  9589  ordtypelem10  9592  oismo  9605  wemapsolem  9615  brwdom2  9638  wdomtr  9640  unwdomg  9649  xpwdomg  9650  unxpwdom2  9653  cantnfval2  9734  cantnfle  9736  cantnflem1  9754  cantnf  9758  r1ordg  9843  tcrank  9949  carddomi2  10035  harval2  10062  infxpenlem  10078  infxpenc2lem2  10085  fseqenlem1  10089  dfac8clem  10097  acndom2  10119  infpwfien  10127  iunfictbso  10179  dfac12lem3  10211  infxp  10279  coflim  10326  cofsmo  10334  coftr  10338  sornom  10342  infpssrlem4  10371  enfin2i  10386  fin23lem26  10390  fin23lem27  10393  fin23lem36  10413  fin23lem40  10416  isf32lem5  10422  isf34lem4  10442  isfin1-3  10451  fin1a2lem10  10474  fin1a2lem13  10477  fin1a2s  10479  hsmexlem4  10494  ttukeylem5  10578  ttukeylem6  10579  ttukeylem7  10580  alephval2  10637  gchor  10692  fpwwe2lem6  10701  fpwwe2lem11  10706  fpwwe2  10708  pwfseqlem4a  10726  pwfseqlem4  10727  winalim2  10761  gchina  10764  inar1  10840  nqereq  11000  prlem934  11098  prlem936  11112  addsrmo  11138  mulsrmo  11139  supsrlem  11176  axpre-sup  11234  dedekind  11449  dedekindle  11450  mulge0b  12161  supaddc  12258  supmul1  12260  un0addcl  12582  un0mulcl  12583  uzwo3  13004  qbtwnre  13257  xlemul1a  13346  seqcl2  14067  seqfveq2  14071  seqshft2  14075  monoord  14079  seqsplit  14082  seqf1olem1  14088  seqid2  14095  seqhomo  14096  expnegz  14143  expcan  14215  ltexp2  14216  discr  14285  bcval5  14363  hashbc  14498  hashf1lem2  14501  seqcoll  14509  seqcoll2  14510  wrdind  14766  wrd2ind  14767  cau3lem  15399  ello1d  15565  lo1bdd2  15566  rlimclim  15588  climrlim2  15589  rlimdm  15593  rlimcn1  15630  reccn2  15639  rlimsqzlem  15693  lo1le  15696  caucvgrlem  15717  caurcvg2  15722  summolem2  15760  zsum  15762  fsum  15764  fsumf1o  15767  sumss  15768  fsumss  15769  fsumcl2lem  15775  fsumadd  15784  fsumcom2  15818  fsum0diag2  15827  fsummulc2  15828  fsumconst  15834  fsumrelem  15851  fsumrlim  15855  fsumo1  15856  divrcnv  15896  geomulcvg  15920  mertenslem2  15929  prodmolem2  15977  zprod  15979  fprod  15983  fprodf1o  15988  prodss  15989  fprodss  15990  fprodcl2lem  15992  fprodmul  16002  fproddiv  16003  fprodconst  16020  fprodn0  16021  fprodcom2  16026  ruclem8  16279  dvds0lem  16309  dvdsnegb  16316  dvdssub2  16343  bitsf1  16486  bitsshft  16515  bezoutlem3  16582  bezoutlem4  16583  isprm5  16748  isprm6  16755  hashgcdeq  16831  modprminv  16841  modprminveq  16842  reumodprminv  16846  pcqmul  16895  pcqcl  16898  pcxnn0cl  16902  pcxcl  16903  pc2dvds  16921  pcadd  16931  pcmpt  16934  pockthg  16948  infpnlem1  16952  prmreclem5  16962  vdwlem2  17024  vdwlem9  17031  vdwlem10  17032  vdwlem12  17034  ramub  17055  0ram  17062  ramub1lem2  17069  ramub1  17070  ramcl  17071  mreexexd  17701  acsfn2  17716  iscatd  17726  catpropd  17762  setcmon  18149  pleval2i  18401  psss  18645  mgmidsssn0  18705  mgmhmeql  18749  mhmeql  18856  frmdss2  18893  frmdup3  18897  grprcan  19008  dfgrp3lem  19073  mulgnn0ass  19145  isnsg3  19195  ghmpreima  19273  ghmeql  19274  gaorber  19343  f1omvdco2  19485  psgnunilem1  19530  psgnunilem2  19532  oddvds  19584  gexdvds  19621  sylow1lem1  19635  odcau  19641  pgpssslw  19651  sylow2alem2  19655  sylow2blem3  19659  fislw  19662  lsmmod  19712  efgredlem  19784  frgpup3  19815  gsumval3  19944  gsumzres  19946  gsumzcl2  19947  gsumzf1o  19949  gsumzaddlem  19958  gsumconst  19971  gsumzmhm  19974  gsumzoppg  19981  gsum2d2lem  20010  ablfac1eulem  20111  pgpfac1lem5  20118  ablfaclem3  20126  issubdrg  20798  lss1d  20979  lmhmeql  21072  lspextmo  21073  lspsnat  21165  lsppratlem6  21172  islbs3  21175  lbsextlem4  21181  lidl1el  21254  cnsubrg  21463  gsumfsum  21470  prmirredlem  21501  znidomb  21598  frgpcyg  21610  cssmre  21729  dsmmsubg  21781  dsmmlss  21782  frlmsslsp  21834  lindff1  21858  lindfrn  21859  rnasclassa  21932  mvrf1  22023  mplsubglem  22036  mpllsslem  22037  mplcoe1  22072  mplcoe5  22075  gsummoncoe1  22326  mat1dimcrng  22497  mdetdiaglem  22618  mdetunilem7  22638  mdetunilem8  22639  mdetunilem9  22640  cpmatacl  22736  cpmatmcllem  22738  mp2pm2mplem4  22829  en2top  23006  toponmre  23115  topssnei  23146  innei  23147  clslp  23170  restcls  23203  restntr  23204  ordtrest2lem  23225  cnpco  23289  cncls2  23295  cncnpi  23300  cncnp  23302  cnconst2  23305  cnpdis  23315  lmcnp  23326  cnhaus  23376  isreg2  23399  cncmp  23414  tgcmp  23423  sscmp  23427  cmpfi  23430  cnconn  23444  iunconnlem  23449  clsconn  23452  1stcfb  23467  1stcrest  23475  2ndcctbss  23477  2ndcdisj  23478  1stcelcls  23483  1stccnp  23484  restnlly  23504  cldllycmp  23517  lly1stc  23518  dislly  23519  locfincmp  23548  comppfsc  23554  kgentopon  23560  kgenidm  23569  1stckgenlem  23575  kgencn3  23580  ptpjpre1  23593  ptbasin  23599  txcls  23626  tx2cn  23632  ptpjcn  23633  ptclsg  23637  ptcnp  23644  txdis  23654  txlly  23658  txnlly  23659  pthaus  23660  txtube  23662  txcmplem1  23663  txcmplem2  23664  txcmp  23665  txhaus  23669  txkgen  23674  xkohaus  23675  xkococnlem  23681  xkococn  23682  txconn  23711  qtopeu  23738  qtoprest  23739  regr1lem2  23762  kqreglem1  23763  cmphaushmeo  23822  xkocnv  23836  fgabs  23901  filuni  23907  trufil  23932  ufileu  23941  filufint  23942  fin1aufil  23954  elfm2  23970  rnelfmlem  23974  fmfnfmlem2  23977  fmfnfmlem4  23979  fmufil  23981  flimopn  23997  fbflim2  23999  hausflimi  24002  hausflim  24003  flimcf  24004  flimclslem  24006  flimsncls  24008  hauspwpwf1  24009  cnpflfi  24021  fclsnei  24041  fclscf  24047  flimfnfcls  24050  fclscmp  24052  ufilcmp  24054  fcfnei  24057  cnpfcf  24063  alexsublem  24066  alexsub  24067  alexsubALTlem2  24070  alexsubALTlem3  24071  alexsubALTlem4  24072  ptcmplem3  24076  ptcmplem4  24077  ptcmplem5  24078  symgtgp  24128  tgpconncompeqg  24134  tgpconncomp  24135  ghmcnp  24137  tgpt0  24141  qustgplem  24143  haustsms2  24159  tsmsgsum  24161  tsmsres  24166  tsmsxp  24177  imasdsf1olem  24397  xbln0  24438  blssps  24448  blss  24449  neibl  24528  blcld  24532  metss  24535  metequiv2  24537  met1stc  24548  metrest  24551  prdsxmslem2  24556  metcnp3  24567  nrmmetd  24601  nlmvscnlem1  24721  nrginvrcnlem  24726  nmoleub  24766  icccmplem2  24857  icccmp  24859  reconnlem2  24861  xrge0tsms  24868  metdstri  24885  metdseq0  24888  metdscn  24890  cnmpopc  24967  lebnumlem3  25007  pcoval2  25061  pcopt  25067  nmoleub2lem  25159  nmhmcn  25165  ipcnlem1  25291  cfilfcls  25320  cmetcaulem  25334  iscmet3lem2  25338  iscmet3  25339  equivcau  25346  caubl  25354  bcthlem2  25371  bcthlem3  25372  bcthlem4  25373  bcthlem5  25374  ivthlem2  25499  ivthlem3  25500  ovoliunlem2  25550  ovolicc2lem2  25565  ovolicc2lem5  25568  ovolicc2  25569  ismbl2  25574  nulmbl  25582  nulmbl2  25583  unmbl  25584  shftmbl  25585  voliunlem3  25599  volsup  25603  ioombl1lem4  25608  ioombl1  25609  icombl  25611  ioombl  25612  uniioombl  25636  opnmbllem  25648  volivth  25654  vitali  25660  mbflimsup  25713  i1fadd  25742  itg1addlem4  25746  itg1addlem4OLD  25747  itg2le  25787  itg2seq  25790  itg2lea  25792  itg2splitlem  25796  itg2split  25797  itg2mono  25801  itg2gt0  25808  itg2cnlem2  25810  itgss  25859  itgfsum  25874  itgcn  25892  ellimc3  25926  limcco  25940  limciun  25941  dvnres  25979  dvnfre  26002  rolle  26040  c1liplem1  26047  dvivth  26061  dvne0  26062  lhop1lem  26064  lhop1  26065  lhop  26067  dvcnvrelem1  26068  dvfsumrlim  26084  dvfsum2  26087  ftc1a  26090  ftc1lem6  26094  itgsubst  26102  tdeglem4  26111  mdegaddle  26125  mdegvscale  26126  mdegmullem  26129  deg1tmle  26169  ply1divex  26188  dvdsq1p  26214  fta1g  26221  fta1b  26223  plyco0  26243  coeeulem  26275  dgrlem  26280  plyco  26292  coemullem  26301  dgreq0  26317  dgrco  26327  plydivex  26349  quotcan  26361  aannenlem1  26380  aalioulem2  26385  aalioulem3  26386  taylthlem1  26425  ulmbdd  26451  itgulm  26461  radcnvlt1  26471  psercnlem1  26479  abelthlem2  26486  abelthlem8  26493  logcnlem5  26697  efopn  26709  cxpmul2z  26742  cxpcn3lem  26799  cxpeq  26809  xrlimcnp  27020  cxplim  27024  o1cxp  27027  cxploglim  27030  scvxcvx  27038  jensen  27041  ftalem1  27125  ftalem2  27126  fta  27132  basellem3  27135  isppw2  27167  ppinprm  27204  chtnprm  27206  mpodvdsmulf1o  27246  dvdsmulf1o  27248  chtublem  27264  perfectlem2  27283  dchrfi  27308  dchrptlem1  27317  dchrptlem2  27318  dchrptlem3  27319  dchrsum2  27321  bposlem1  27337  bposlem3  27339  2sqlem5  27475  2sqlem6  27476  2sqlem8  27479  2sqlem10  27481  2sqb  27485  chebbnd1lem1  27522  chtppilimlem2  27527  dchrisum0flb  27563  dchrisum0fno1  27564  dchrisum0  27573  pntrsumbnd2  27620  pntpbnd1  27639  pntpbnd2  27640  pntlemp  27663  pnt3  27665  qabvle  27678  ostth2lem2  27687  ostth3  27691  ostth  27692  nolt02o  27749  nogt01o  27750  nosupprefixmo  27754  noinfprefixmo  27755  nosupbnd1lem3  27764  nosupbnd1lem4  27765  nosupbnd1lem5  27766  noinfbnd1lem3  27779  noinfbnd1lem4  27780  noinfbnd1lem5  27781  noetasuplem4  27790  noetainflem4  27794  etasslt  27867  cuteq1  27887  madebdaylemlrcut  27946  cutlt  27975  mulsuniflem  28184  om2noseqlt  28314  readdscl  28440  remulscl  28443  colinearalglem4  28933  axcontlem10  28997  upgrex  29118  smcnlem  30720  ubthlem1  30893  ubthlem3  30895  htthlem  30940  5oalem6  31682  leopmuli  32156  pjnormssi  32191  pjclem4  32222  pj3si  32230  hatomistici  32385  sumdmdlem  32441  wrdt2ind  32912  xrge0tsmsd  33033  isarchiofld  33304  ordtrest2NEWlem  33860  qqhf  33924  eulerpartlemb  34325  ballotlemfc0  34449  ballotlemfcc  34450  sgn3da  34498  subfacp1lem5  35144  erdszelem7  35157  erdszelem11  35161  pconnconn  35191  txpconn  35192  connpconn  35195  sconnpi1  35199  txsconn  35201  cvxsconn  35203  cvmopnlem  35238  cvmfolem  35239  cvmliftmolem2  35242  cvmliftlem7  35251  cvmliftlem10  35254  cvmlift2lem10  35272  cvmlift3lem4  35282  cvmlift3lem8  35286  satfun  35371  msubff1  35516  wzel  35780  wsuclem  35781  btwnouttr2  35978  cgrxfr  36011  btwnxfr  36012  brcolinear  36015  lineext  36032  btwnconn1lem13  36055  midofsegid  36060  segcon2  36061  brsegle  36064  seglecgr12im  36066  segletr  36070  colinbtwnle  36074  broutsideof2  36078  btwnoutside  36081  broutsideof3  36082  outsideoftr  36085  outsideofeq  36086  outsideofeu  36087  outsidele  36088  lineunray  36103  lineelsb2  36104  linethru  36109  finminlem  36231  nn0prpwlem  36235  neibastop2lem  36273  neibastop2  36274  neibastop3  36275  topjoin  36278  tailfb  36290  relowlssretop  37277  fvineqsneq  37326  wl-sbcom2d-lem1  37461  finixpnum  37513  poimirlem6  37534  poimirlem7  37535  poimirlem13  37541  poimirlem26  37554  poimirlem29  37557  heicant  37563  opnmbllem0  37564  mblfinlem3  37567  ismblfin  37569  ovoliunnfl  37570  voliunnfl  37572  volsupnfl  37573  itg2addnclem  37579  itg2addnclem3  37581  ftc1cnnc  37600  sdclem2  37650  fdc  37653  istotbnd3  37679  isbnd2  37691  isbnd3  37692  prdsbnd  37701  cntotbnd  37704  heibor1lem  37717  heibor1  37718  heiborlem10  37728  rrncmslem  37740  ghomco  37799  1idl  37934  unichnidl  37939  disjlem18  38704  prtlem10  38769  prtlem18  38781  atlatmstc  39223  cvrexchlem  39324  paddasslem14  39738  pexmidlem5N  39879  cdleme29ex  40279  cdlemefr29exN  40307  cdleme32fva  40342  diarnN  41034  dihlsscpre  41139  isnacs3  42603  fnwe2lem2  42948  kelac1  42960  hbtlem5  43025  hbt  43027  dgraa0p  43046  ofoafg  43256  ofoafo  43258  naddcnffo  43266  fzunt  43357  fzuntd  43358  monoordxrv  45331  rlimdmafv  47024  rlimdmafv2  47105  fmtnoprmfac2  47373  perfectALTVlem2  47528  mogoldbb  47591  lindslinindsimp2  48110