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  3134  reximddv  3148  disjxiun  5086  wereu2  5611  frpomin  6287  ordtr3  6352  fcof1  7221  knatar  7291  riota5f  7331  ovmpodf  7502  extmptsuppeq  8118  suppss  8124  suppss2  8130  frrlem14  8229  fprresex  8240  smoord  8285  tfrlem9a  8305  oaass  8476  oelimcl  8515  oaabs2  8564  cofon1  8587  naddssim  8600  swoso  8656  eceqoveq  8746  domdifsn  8973  domunsncan  8990  omxpenlem  8991  enfixsn  8999  mapdom2  9061  frfi  9169  fofinf1o  9216  finsschain  9243  elfiun  9314  marypha1lem  9317  eqsupd  9341  eqinfd  9370  ordiso2  9401  ordtypelem6  9409  ordtypelem7  9410  ordtypelem10  9413  oismo  9426  wemapsolem  9436  brwdom2  9459  wdomtr  9461  unwdomg  9470  xpwdomg  9471  unxpwdom2  9474  cantnfval2  9559  cantnfle  9561  cantnflem1  9579  cantnf  9583  r1ordg  9671  tcrank  9777  carddomi2  9863  harval2  9890  infxpenlem  9904  infxpenc2lem2  9911  fseqenlem1  9915  dfac8clem  9923  acndom2  9945  infpwfien  9953  iunfictbso  10005  dfac12lem3  10037  infxp  10105  coflim  10152  cofsmo  10160  coftr  10164  sornom  10168  infpssrlem4  10197  enfin2i  10212  fin23lem26  10216  fin23lem27  10219  fin23lem36  10239  fin23lem40  10242  isf32lem5  10248  isf34lem4  10268  isfin1-3  10277  fin1a2lem10  10300  fin1a2lem13  10303  fin1a2s  10305  hsmexlem4  10320  ttukeylem5  10404  ttukeylem6  10405  ttukeylem7  10406  alephval2  10463  gchor  10518  fpwwe2lem6  10527  fpwwe2lem11  10532  fpwwe2  10534  pwfseqlem4a  10552  pwfseqlem4  10553  winalim2  10587  gchina  10590  inar1  10666  nqereq  10826  prlem934  10924  prlem936  10938  addsrmo  10964  mulsrmo  10965  supsrlem  11002  axpre-sup  11060  dedekind  11276  dedekindle  11277  mulge0b  11992  supaddc  12089  supmul1  12091  un0addcl  12414  un0mulcl  12415  uzwo3  12841  qbtwnre  13098  xlemul1a  13187  seqcl2  13927  seqfveq2  13931  seqshft2  13935  monoord  13939  seqsplit  13942  seqf1olem1  13948  seqid2  13955  seqhomo  13956  expnegz  14003  expcan  14076  ltexp2  14077  discr  14147  bcval5  14225  hashbc  14360  hashf1lem2  14363  seqcoll  14371  seqcoll2  14372  wrdind  14629  wrd2ind  14630  cau3lem  15262  ello1d  15430  lo1bdd2  15431  rlimclim  15453  climrlim2  15454  rlimdm  15458  rlimcn1  15495  reccn2  15504  rlimsqzlem  15556  lo1le  15559  caucvgrlem  15580  caurcvg2  15585  summolem2  15623  zsum  15625  fsum  15627  fsumf1o  15630  sumss  15631  fsumss  15632  fsumcl2lem  15638  fsumadd  15647  fsumcom2  15681  fsum0diag2  15690  fsummulc2  15691  fsumconst  15697  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  divrcnv  15759  geomulcvg  15783  mertenslem2  15792  prodmolem2  15842  zprod  15844  fprod  15848  fprodf1o  15853  prodss  15854  fprodss  15855  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodconst  15885  fprodn0  15886  fprodcom2  15891  ruclem8  16146  dvds0lem  16177  dvdsnegb  16184  dvdssub2  16212  bitsf1  16357  bitsshft  16386  bezoutlem3  16452  bezoutlem4  16453  isprm5  16618  isprm6  16625  hashgcdeq  16701  modprminv  16711  modprminveq  16712  reumodprminv  16716  pcqmul  16765  pcqcl  16768  pcxnn0cl  16772  pcxcl  16773  pc2dvds  16791  pcadd  16801  pcmpt  16804  pockthg  16818  infpnlem1  16822  prmreclem5  16832  vdwlem2  16894  vdwlem9  16901  vdwlem10  16902  vdwlem12  16904  ramub  16925  0ram  16932  ramub1lem2  16939  ramub1  16940  ramcl  16941  mreexexd  17554  acsfn2  17569  iscatd  17579  catpropd  17615  setcmon  17994  pleval2i  18240  psss  18486  mgmidsssn0  18580  mgmhmeql  18624  mhmeql  18734  frmdss2  18771  frmdup3  18775  grprcan  18886  dfgrp3lem  18951  mulgnn0ass  19023  isnsg3  19072  ghmpreima  19150  ghmeql  19151  gaorber  19220  f1omvdco2  19360  psgnunilem1  19405  psgnunilem2  19407  oddvds  19459  gexdvds  19496  sylow1lem1  19510  odcau  19516  pgpssslw  19526  sylow2alem2  19530  sylow2blem3  19534  fislw  19537  lsmmod  19587  efgredlem  19659  frgpup3  19690  gsumval3  19819  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  gsum2d2lem  19885  ablfac1eulem  19986  pgpfac1lem5  19993  ablfaclem3  20001  issubdrg  20695  lss1d  20896  lmhmeql  20989  lspextmo  20990  lspsnat  21082  lsppratlem6  21089  islbs3  21092  lbsextlem4  21098  lidl1el  21163  cnsubrg  21364  gsumfsum  21371  prmirredlem  21409  znidomb  21498  frgpcyg  21510  cssmre  21630  dsmmsubg  21680  dsmmlss  21681  frlmsslsp  21733  lindff1  21757  lindfrn  21758  rnasclassa  21832  mvrf1  21923  mplsubglem  21936  mpllsslem  21937  mplcoe1  21972  mplcoe5  21975  gsummoncoe1  22223  mat1dimcrng  22392  mdetdiaglem  22513  mdetunilem7  22533  mdetunilem8  22534  mdetunilem9  22535  cpmatacl  22631  cpmatmcllem  22633  mp2pm2mplem4  22724  en2top  22900  toponmre  23008  topssnei  23039  innei  23040  clslp  23063  restcls  23096  restntr  23097  ordtrest2lem  23118  cnpco  23182  cncls2  23188  cncnpi  23193  cncnp  23195  cnconst2  23198  cnpdis  23208  lmcnp  23219  cnhaus  23269  isreg2  23292  cncmp  23307  tgcmp  23316  sscmp  23320  cmpfi  23323  cnconn  23337  iunconnlem  23342  clsconn  23345  1stcfb  23360  1stcrest  23368  2ndcctbss  23370  2ndcdisj  23371  1stcelcls  23376  1stccnp  23377  restnlly  23397  cldllycmp  23410  lly1stc  23411  dislly  23412  locfincmp  23441  comppfsc  23447  kgentopon  23453  kgenidm  23462  1stckgenlem  23468  kgencn3  23473  ptpjpre1  23486  ptbasin  23492  txcls  23519  tx2cn  23525  ptpjcn  23526  ptclsg  23530  ptcnp  23537  txdis  23547  txlly  23551  txnlly  23552  pthaus  23553  txtube  23555  txcmplem1  23556  txcmplem2  23557  txcmp  23558  txhaus  23562  txkgen  23567  xkohaus  23568  xkococnlem  23574  xkococn  23575  txconn  23604  qtopeu  23631  qtoprest  23632  regr1lem2  23655  kqreglem1  23656  cmphaushmeo  23715  xkocnv  23729  fgabs  23794  filuni  23800  trufil  23825  ufileu  23834  filufint  23835  fin1aufil  23847  elfm2  23863  rnelfmlem  23867  fmfnfmlem2  23870  fmfnfmlem4  23872  fmufil  23874  flimopn  23890  fbflim2  23892  hausflimi  23895  hausflim  23896  flimcf  23897  flimclslem  23899  flimsncls  23901  hauspwpwf1  23902  cnpflfi  23914  fclsnei  23934  fclscf  23940  flimfnfcls  23943  fclscmp  23945  ufilcmp  23947  fcfnei  23950  cnpfcf  23956  alexsublem  23959  alexsub  23960  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem3  23969  ptcmplem4  23970  ptcmplem5  23971  symgtgp  24021  tgpconncompeqg  24027  tgpconncomp  24028  ghmcnp  24030  tgpt0  24034  qustgplem  24036  haustsms2  24052  tsmsgsum  24054  tsmsres  24059  tsmsxp  24070  imasdsf1olem  24288  xbln0  24329  blssps  24339  blss  24340  neibl  24416  blcld  24420  metss  24423  metequiv2  24425  met1stc  24436  metrest  24439  prdsxmslem2  24444  metcnp3  24455  nrmmetd  24489  nlmvscnlem1  24601  nrginvrcnlem  24606  nmoleub  24646  icccmplem2  24739  icccmp  24741  reconnlem2  24743  xrge0tsms  24750  metdstri  24767  metdseq0  24770  metdscn  24772  cnmpopc  24849  lebnumlem3  24889  pcoval2  24943  pcopt  24949  nmoleub2lem  25041  nmhmcn  25047  ipcnlem1  25172  cfilfcls  25201  cmetcaulem  25215  iscmet3lem2  25219  iscmet3  25220  equivcau  25227  caubl  25235  bcthlem2  25252  bcthlem3  25253  bcthlem4  25254  bcthlem5  25255  ivthlem2  25380  ivthlem3  25381  ovoliunlem2  25431  ovolicc2lem2  25446  ovolicc2lem5  25449  ovolicc2  25450  ismbl2  25455  nulmbl  25463  nulmbl2  25464  unmbl  25465  shftmbl  25466  voliunlem3  25480  volsup  25484  ioombl1lem4  25489  ioombl1  25490  icombl  25492  ioombl  25493  uniioombl  25517  opnmbllem  25529  volivth  25535  vitali  25541  mbflimsup  25594  i1fadd  25623  itg1addlem4  25627  itg2le  25667  itg2seq  25670  itg2lea  25672  itg2splitlem  25676  itg2split  25677  itg2mono  25681  itg2gt0  25688  itg2cnlem2  25690  itgss  25740  itgfsum  25755  itgcn  25773  ellimc3  25807  limcco  25821  limciun  25822  dvnres  25860  dvnfre  25883  rolle  25921  c1liplem1  25928  dvivth  25942  dvne0  25943  lhop1lem  25945  lhop1  25946  lhop  25948  dvcnvrelem1  25949  dvfsumrlim  25965  dvfsum2  25968  ftc1a  25971  ftc1lem6  25975  itgsubst  25983  tdeglem4  25992  mdegaddle  26006  mdegvscale  26007  mdegmullem  26010  deg1tmle  26050  ply1divex  26069  dvdsq1p  26095  fta1g  26102  fta1b  26104  plyco0  26124  coeeulem  26156  dgrlem  26161  plyco  26173  coemullem  26182  dgreq0  26198  dgrco  26208  plydivex  26232  quotcan  26244  aannenlem1  26263  aalioulem2  26268  aalioulem3  26269  taylthlem1  26308  ulmbdd  26334  itgulm  26344  radcnvlt1  26354  psercnlem1  26362  abelthlem2  26369  abelthlem8  26376  logcnlem5  26582  efopn  26594  cxpmul2z  26627  cxpcn3lem  26684  cxpeq  26694  xrlimcnp  26905  cxplim  26909  o1cxp  26912  cxploglim  26915  scvxcvx  26923  jensen  26926  ftalem1  27010  ftalem2  27011  fta  27017  basellem3  27020  isppw2  27052  ppinprm  27089  chtnprm  27091  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chtublem  27149  perfectlem2  27168  dchrfi  27193  dchrptlem1  27202  dchrptlem2  27203  dchrptlem3  27204  dchrsum2  27206  bposlem1  27222  bposlem3  27224  2sqlem5  27360  2sqlem6  27361  2sqlem8  27364  2sqlem10  27366  2sqb  27370  chebbnd1lem1  27407  chtppilimlem2  27412  dchrisum0flb  27448  dchrisum0fno1  27449  dchrisum0  27458  pntrsumbnd2  27505  pntpbnd1  27524  pntpbnd2  27525  pntlemp  27548  pnt3  27550  qabvle  27563  ostth2lem2  27572  ostth3  27576  ostth  27577  nolt02o  27634  nogt01o  27635  nosupprefixmo  27639  noinfprefixmo  27640  nosupbnd1lem3  27649  nosupbnd1lem4  27650  nosupbnd1lem5  27651  noinfbnd1lem3  27664  noinfbnd1lem4  27665  noinfbnd1lem5  27666  noetasuplem4  27675  noetainflem4  27679  etasslt  27754  cuteq1  27778  madebdaylemlrcut  27844  cutlt  27876  mulsuniflem  28088  bdayon  28209  om2noseqlt  28229  n0sfincut  28282  zs12ge0  28393  readdscl  28401  remulscl  28404  colinearalglem4  28887  axcontlem10  28951  upgrex  29070  smcnlem  30677  ubthlem1  30850  ubthlem3  30852  htthlem  30897  5oalem6  31639  leopmuli  32113  pjnormssi  32148  pjclem4  32179  pj3si  32187  hatomistici  32342  sumdmdlem  32398  sgn3da  32817  wrdt2ind  32934  xrge0tsmsd  33042  isarchiofld  33168  ordtrest2NEWlem  33935  qqhf  33999  eulerpartlemb  34381  ballotlemfc0  34506  ballotlemfcc  34507  subfacp1lem5  35228  erdszelem7  35241  erdszelem11  35245  pconnconn  35275  txpconn  35276  connpconn  35279  sconnpi1  35283  txsconn  35285  cvxsconn  35287  cvmopnlem  35322  cvmfolem  35323  cvmliftmolem2  35326  cvmliftlem7  35335  cvmliftlem10  35338  cvmlift2lem10  35356  cvmlift3lem4  35366  cvmlift3lem8  35370  satfun  35455  msubff1  35600  wzel  35866  wsuclem  35867  btwnouttr2  36066  cgrxfr  36099  btwnxfr  36100  brcolinear  36103  lineext  36120  btwnconn1lem13  36143  midofsegid  36148  segcon2  36149  brsegle  36152  seglecgr12im  36154  segletr  36158  colinbtwnle  36162  broutsideof2  36166  btwnoutside  36169  broutsideof3  36170  outsideoftr  36173  outsideofeq  36174  outsideofeu  36175  outsidele  36176  lineunray  36191  lineelsb2  36192  linethru  36197  finminlem  36362  nn0prpwlem  36366  neibastop2lem  36404  neibastop2  36405  neibastop3  36406  topjoin  36409  tailfb  36421  relowlssretop  37407  fvineqsneq  37456  wl-sbcom2d-lem1  37603  finixpnum  37655  poimirlem6  37676  poimirlem7  37677  poimirlem13  37683  poimirlem26  37696  poimirlem29  37699  heicant  37705  opnmbllem0  37706  mblfinlem3  37709  ismblfin  37711  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  itg2addnclem  37721  itg2addnclem3  37723  ftc1cnnc  37742  sdclem2  37792  fdc  37795  istotbnd3  37821  isbnd2  37833  isbnd3  37834  prdsbnd  37843  cntotbnd  37846  heibor1lem  37859  heibor1  37860  heiborlem10  37870  rrncmslem  37882  ghomco  37941  1idl  38076  unichnidl  38081  disjlem18  38908  prtlem10  38974  prtlem18  38986  atlatmstc  39428  cvrexchlem  39528  paddasslem14  39942  pexmidlem5N  40083  cdleme29ex  40483  cdlemefr29exN  40511  cdleme32fva  40546  diarnN  41238  dihlsscpre  41343  isnacs3  42813  fnwe2lem2  43154  kelac1  43166  hbtlem5  43231  hbt  43233  dgraa0p  43252  ofoafg  43457  ofoafo  43459  naddcnffo  43467  fzunt  43558  fzuntd  43559  monoordxrv  45589  rlimdmafv  47287  rlimdmafv2  47368  fmtnoprmfac2  47677  perfectALTVlem2  47832  mogoldbb  47895  lindslinindsimp2  48574