Theorem expr 461

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  animpimp2impd  859  3expia  1139  rexlimdvaa  3167  reximddv  3181  disjxiun  5106  wereu2  5658  frpomin  6341  ordtr3  6407  fcof1  7285  knatar  7355  riota5f  7395  ovmpodf  7566  extmptsuppeq  8180  suppss  8186  suppss2  8192  frrlem14  8292  fprresex  8303  smoord  8348  tfrlem9a  8369  oaass  8542  oelimcl  8582  oaabs2  8631  cofon1  8654  naddssim  8668  swoso  8725  eceqoveq  8816  domdifsn  9044  domunsncan  9061  omxpenlem  9062  enfixsn  9070  mapdom2  9132  frfi  9241  fofinf1o  9285  finsschain  9312  elfiun  9386  marypha1lem  9389  eqsupd  9413  eqinfd  9442  ordiso2  9473  ordtypelem6  9481  ordtypelem7  9482  ordtypelem10  9485  oismo  9498  wemapsolem  9508  brwdom2  9531  wdomtr  9533  unwdomg  9542  xpwdomg  9543  unxpwdom2  9546  cantnfval2  9634  cantnfle  9636  cantnflem1  9654  cantnf  9658  r1ordg  9746  tcrank  9852  carddomi2  9952  harval2  9979  infxpenlem  9993  infxpenc2lem2  10000  fseqenlem1  10004  dfac8clem  10012  acndom2  10034  infpwfien  10042  iunfictbso  10094  dfac12lem3  10125  infxp  10193  coflim  10240  cofsmo  10248  coftr  10252  sornom  10256  infpssrlem4  10285  enfin2i  10300  fin23lem26  10304  fin23lem27  10307  fin23lem36  10327  fin23lem40  10330  isf32lem5  10336  isf34lem4  10356  isfin1-3  10365  fin1a2lem10  10388  fin1a2lem13  10391  fin1a2s  10393  hsmexlem4  10408  ttukeylem5  10492  ttukeylem6  10493  ttukeylem7  10494  alephval2  10552  gchor  10607  fpwwe2lem6  10616  fpwwe2lem11  10621  fpwwe2  10623  pwfseqlem4a  10641  pwfseqlem4  10642  winalim2  10676  gchina  10679  inar1  10755  nqereq  10915  prlem934  11013  prlem936  11027  addsrmo  11053  mulsrmo  11054  supsrlem  11091  axpre-sup  11149  dedekind  11368  dedekindle  11369  mulge0b  12080  supaddc  12177  supmul1  12179  un0addcl  12532  un0mulcl  12533  uzwo3  12962  qbtwnre  13220  xlemul1a  13309  seqcl2  14052  seqfveq2  14056  seqshft2  14060  monoord  14064  seqsplit  14067  seqf1olem1  14073  seqid2  14080  seqhomo  14081  expnegz  14128  expcan  14201  ltexp2  14202  discr  14272  bcval5  14350  hashbc  14486  hashf1lem2  14489  seqcoll  14497  seqcoll2  14498  wrdind  14755  wrd2ind  14756  sgn3da  15134  cau3lem  15402  ello1d  15570  lo1bdd2  15571  rlimclim  15593  climrlim2  15594  rlimdm  15598  rlimcn1  15635  reccn2  15644  rlimsqzlem  15696  lo1le  15699  caucvgrlem  15720  caurcvg2  15725  summolem2  15763  zsum  15765  fsum  15767  fsumf1o  15770  sumss  15771  fsumss  15772  fsumcl2lem  15778  fsumadd  15787  fsumcom2  15821  fsum0diag2  15830  fsummulc2  15831  fsumconst  15837  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  divrcnv  15902  geomulcvg  15926  mertenslem2  15935  prodmolem2  15985  zprod  15987  fprod  15991  fprodf1o  15996  prodss  15997  fprodss  15998  fprodcl2lem  16000  fprodmul  16010  fproddiv  16011  fprodconst  16028  fprodn0  16029  fprodcom2  16034  ruclem8  16288  dvds0lem  16319  dvdsnegb  16326  dvdssub2  16354  bitsf1  16499  bitsshft  16528  bezoutlem3  16594  bezoutlem4  16595  isprm5  16761  isprm6  16768  hashgcdeq  16844  modprminv  16854  modprminveq  16855  reumodprminv  16859  pcqmul  16908  pcqcl  16911  pcxnn0cl  16915  pcxcl  16916  pc2dvds  16934  pcadd  16944  pcmpt  16947  pockthg  16961  infpnlem1  16965  prmreclem5  16975  vdwlem2  17037  vdwlem9  17044  vdwlem10  17045  vdwlem12  17047  ramub  17068  0ram  17075  ramub1lem2  17082  ramub1  17083  ramcl  17084  mreexexd  17699  acsfn2  17714  iscatd  17724  catpropd  17760  setcmon  18139  pleval2i  18385  psss  18631  mgmidsssn0  18725  mgmhmeql  18769  mhmeql  18880  frmdss2  18917  frmdup3  18921  grprcan  19035  dfgrp3lem  19099  mulgnn0ass  19171  isnsg3  19221  ghmpreima  19303  ghmeql  19304  gaorber  19373  f1omvdco2  19513  psgnunilem1  19558  psgnunilem2  19560  oddvds  19612  gexdvds  19649  sylow1lem1  19663  odcau  19669  pgpssslw  19679  sylow2alem2  19683  sylow2blem3  19687  fislw  19690  lsmmod  19740  efgredlem  19812  frgpup3  19843  gsumval3  19972  gsumzres  19974  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  gsumzoppg  20009  gsum2d2lem  20038  ablfac1eulem  20139  pgpfac1lem5  20146  ablfaclem3  20154  issubdrg  20883  lss1d  21084  lmhmeql  21176  lspextmo  21177  lspsnat  21269  lsppratlem6  21276  islbs3  21279  lbsextlem4  21285  lidl1el  21351  cnsubrg  21577  gsumfsum  21584  prmirredlem  21622  znidomb  21711  frgpcyg  21723  cssmre  21843  dsmmsubg  21893  dsmmlss  21894  frlmsslsp  21946  lindff1  21970  lindfrn  21971  rnasclassa  22045  mvrf1  22135  mplsubglem  22148  mpllsslem  22149  mplcoe1  22188  mplcoe5  22191  gsummoncoe1  22468  mat1dimcrng  22634  mdetdiaglem  22755  mdetunilem7  22775  mdetunilem8  22776  mdetunilem9  22777  cpmatacl  22873  cpmatmcllem  22875  mp2pm2mplem4  22966  en2top  23142  toponmre  23250  topssnei  23281  innei  23282  clslp  23305  restcls  23338  restntr  23339  ordtrest2lem  23360  cnpco  23424  cncls2  23430  cncnpi  23435  cncnp  23437  cnconst2  23440  cnpdis  23450  lmcnp  23461  cnhaus  23511  isreg2  23534  cncmp  23549  tgcmp  23558  sscmp  23562  cmpfi  23565  cnconn  23579  iunconnlem  23584  clsconn  23587  1stcfb  23602  1stcrest  23610  2ndcctbss  23612  2ndcdisj  23613  1stcelcls  23618  1stccnp  23619  restnlly  23639  cldllycmp  23652  lly1stc  23653  dislly  23654  locfincmp  23683  comppfsc  23689  kgentopon  23695  kgenidm  23704  1stckgenlem  23710  kgencn3  23715  ptpjpre1  23728  ptbasin  23734  txcls  23761  tx2cn  23767  ptpjcn  23768  ptclsg  23772  ptcnp  23779  txdis  23789  txlly  23793  txnlly  23794  pthaus  23795  txtube  23797  txcmplem1  23798  txcmplem2  23799  txcmp  23800  txhaus  23804  txkgen  23809  xkohaus  23810  xkococnlem  23816  xkococn  23817  txconn  23846  qtopeu  23873  qtoprest  23874  regr1lem2  23897  kqreglem1  23898  cmphaushmeo  23957  xkocnv  23971  fgabs  24036  filuni  24042  trufil  24067  ufileu  24076  filufint  24077  fin1aufil  24089  elfm2  24105  rnelfmlem  24109  fmfnfmlem2  24112  fmfnfmlem4  24114  fmufil  24116  flimopn  24132  fbflim2  24134  hausflimi  24137  hausflim  24138  flimcf  24139  flimclslem  24141  flimsncls  24143  hauspwpwf1  24144  cnpflfi  24156  fclsnei  24176  fclscf  24182  flimfnfcls  24185  fclscmp  24187  ufilcmp  24189  fcfnei  24192  cnpfcf  24198  alexsublem  24201  alexsub  24202  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem3  24211  ptcmplem4  24212  ptcmplem5  24213  symgtgp  24263  tgpconncompeqg  24269  tgpconncomp  24270  ghmcnp  24272  tgpt0  24276  qustgplem  24278  haustsms2  24294  tsmsgsum  24296  tsmsres  24301  tsmsxp  24312  imasdsf1olem  24530  xbln0  24571  blssps  24581  blss  24582  neibl  24658  blcld  24662  metss  24665  metequiv2  24667  met1stc  24678  metrest  24681  prdsxmslem2  24686  metcnp3  24697  nrmmetd  24731  nlmvscnlem1  24843  nrginvrcnlem  24848  nmoleub  24888  icccmplem2  24981  icccmp  24983  reconnlem2  24985  xrge0tsms  24992  metdstri  25009  metdseq0  25012  metdscn  25014  cnmpopc  25087  lebnumlem3  25122  pcoval2  25175  pcopt  25181  nmoleub2lem  25273  nmhmcn  25279  ipcnlem1  25404  cfilfcls  25433  cmetcaulem  25447  iscmet3lem2  25451  iscmet3  25452  equivcau  25459  caubl  25467  bcthlem2  25484  bcthlem3  25485  bcthlem4  25486  bcthlem5  25487  ivthlem2  25611  ivthlem3  25612  ovoliunlem2  25662  ovolicc2lem2  25677  ovolicc2lem5  25680  ovolicc2  25681  ismbl2  25686  nulmbl  25694  nulmbl2  25695  unmbl  25696  shftmbl  25697  voliunlem3  25711  volsup  25715  ioombl1lem4  25720  ioombl1  25721  icombl  25723  ioombl  25724  uniioombl  25748  opnmbllem  25760  volivth  25766  vitali  25772  mbflimsup  25825  i1fadd  25854  itg1addlem4  25858  itg2le  25898  itg2seq  25901  itg2lea  25903  itg2splitlem  25907  itg2split  25908  itg2mono  25912  itg2gt0  25919  itg2cnlem2  25921  itgss  25971  itgfsum  25986  itgcn  26004  ellimc3  26038  limcco  26052  limciun  26053  dvnres  26090  dvnfre  26111  rolle  26149  c1liplem1  26155  dvivth  26169  dvne0  26170  lhop1lem  26172  lhop1  26173  lhop  26175  dvcnvrelem1  26176  dvfsumrlim  26190  dvfsum2  26193  ftc1a  26196  ftc1lem6  26200  itgsubst  26208  tdeglem4  26217  mdegaddle  26231  mdegvscale  26232  mdegmullem  26235  deg1tmle  26275  ply1divex  26294  dvdsq1p  26320  fta1g  26327  fta1b  26329  plyco0  26349  coeeulem  26381  dgrlem  26386  plyco  26398  coemullem  26407  dgreq0  26422  dgrco  26432  plydivex  26458  quotcan  26470  aannenlem1  26491  aalioulem2  26496  aalioulem3  26497  taylthlem1  26536  ulmbdd  26561  itgulm  26571  radcnvlt1  26581  psercnlem1  26588  abelthlem2  26595  abelthlem8  26602  logcnlem5  26811  efopn  26823  cxpmul2z  26856  cxpcn3lem  26912  cxpeq  26922  xrlimcnp  27133  cxplim  27136  o1cxp  27139  cxploglim  27142  scvxcvx  27150  jensen  27153  ftalem1  27237  ftalem2  27238  fta  27244  basellem3  27247  isppw2  27279  ppinprm  27316  chtnprm  27318  mpodvdsmulf1o  27358  dvdsmulf1o  27360  chtublem  27375  perfectlem2  27394  dchrfi  27419  dchrptlem1  27428  dchrptlem2  27429  dchrptlem3  27430  dchrsum2  27432  bposlem1  27448  bposlem3  27450  2sqlem5  27586  2sqlem6  27587  2sqlem8  27590  2sqlem10  27592  2sqb  27596  chebbnd1lem1  27633  chtppilimlem2  27638  dchrisum0flb  27674  dchrisum0fno1  27675  dchrisum0  27684  pntrsumbnd2  27731  pntpbnd1  27750  pntpbnd2  27751  pntlemp  27774  pnt3  27776  qabvle  27789  ostth2lem2  27798  ostth3  27802  ostth  27803  nolt02o  27859  nogt01o  27860  nosupprefixmo  27864  noinfprefixmo  27865  nosupbnd1lem3  27874  nosupbnd1lem4  27875  nosupbnd1lem5  27876  noinfbnd1lem3  27889  noinfbnd1lem4  27890  noinfbnd1lem5  27891  noetasuplem4  27900  noetainflem4  27904  etaslts  27986  cuteq1  28010  madebdaylemlrcut  28092  cutlt  28125  mulsuniflem  28342  bdayons  28469  addonbday  28472  om2noseqlt  28492  n0fincut  28548  bdaypw2n0bndlem  28656  bdayfinbndlem1  28660  z12sge0  28676  readdscl  28692  remulscl  28695  colinearalglem4  29259  axcontlem10  29323  upgrex  29442  smcnlem  31049  ubthlem1  31222  ubthlem3  31224  htthlem  31269  5oalem6  32011  leopmuli  32485  pjnormssi  32520  pjclem4  32551  pj3si  32559  hatomistici  32714  sumdmdlem  32770  wrdt2ind  33273  xrge0tsmsd  33393  isarchiofld  33519  ordtrest2NEWlem  34312  qqhf  34376  eulerpartlemb  34758  ballotlemfc0  34883  ballotlemfcc  34884  subfacp1lem5  35676  erdszelem7  35689  erdszelem11  35693  pconnconn  35723  txpconn  35724  connpconn  35727  sconnpi1  35731  txsconn  35733  cvxsconn  35735  cvmopnlem  35770  cvmfolem  35771  cvmliftmolem2  35774  cvmliftlem7  35783  cvmliftlem10  35786  cvmlift2lem10  35804  cvmlift3lem4  35814  cvmlift3lem8  35818  satfun  35903  msubff1  36048  wzel  36314  wsuclem  36315  btwnouttr2  36514  cgrxfr  36547  btwnxfr  36548  brcolinear  36551  lineext  36568  btwnconn1lem13  36591  midofsegid  36596  segcon2  36597  brsegle  36600  seglecgr12im  36602  segletr  36606  colinbtwnle  36610  broutsideof2  36614  btwnoutside  36617  broutsideof3  36618  outsideoftr  36621  outsideofeq  36622  outsideofeu  36623  outsidele  36624  lineunray  36639  lineelsb2  36640  linethru  36645  nmulrid  36689  nmuladdss  36705  nadddilem1  36712  finminlem  36849  nn0prpwlem  36853  neibastop2lem  36891  neibastop2  36892  neibastop3  36893  topjoin  36896  tailfb  36908  axtcond  37009  relowlssretop  38029  fvineqsneq  38078  wl-sbcom2d-lem1  38234  finixpnum  38276  poimirlem6  38297  poimirlem7  38298  poimirlem13  38304  poimirlem26  38317  poimirlem29  38320  heicant  38326  opnmbllem0  38327  mblfinlem3  38330  ismblfin  38332  ovoliunnfl  38333  voliunnfl  38335  volsupnfl  38336  itg2addnclem  38342  itg2addnclem3  38344  ftc1cnnc  38363  sdclem2  38413  fdc  38416  istotbnd3  38442  isbnd2  38454  isbnd3  38455  prdsbnd  38464  cntotbnd  38467  heibor1lem  38480  heibor1  38481  heiborlem10  38491  rrncmslem  38503  ghomco  38562  1idl  38697  unichnidl  38702  disjlem18  39572  prtlem10  39659  prtlem18  39671  atlatmstc  40113  cvrexchlem  40213  paddasslem14  40627  pexmidlem5N  40768  cdleme29ex  41168  cdlemefr29exN  41196  cdleme32fva  41231  diarnN  41923  dihlsscpre  42028  isnacs3  43461  fnwe2lem2  43798  kelac1  43810  hbtlem5  43875  hbt  43877  dgraa0p  43896  ofoafg  44101  ofoafo  44103  naddcnffo  44111  fzunt  44201  fzuntd  44202  monoordxrv  46215  rlimdmafv  47934  rlimdmafv2  48015  fmtnoprmfac2  48339  perfectALTVlem2  48507  mogoldbb  48570  lindslinindsimp2  49263