Theorem expr 462

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  animpimp2impd  860  3expia  1139  rexlimdvaa  3168  reximddv  3182  disjxiun  5103  wereu2  5652  frpomin  6350  ordtr3  6416  fcof1  7305  knatar  7377  riota5f  7415  ovmpodf  7586  fnwe2lem3  8160  extmptsuppeq  8219  suppss  8225  suppss2  8231  frrlem14  8331  fprresex  8342  smoord  8387  tfrlem9a  8408  oaass  8583  oelimcl  8623  oaabs2  8672  cofon1  8695  naddssim  8709  swoso  8766  eceqoveq  8857  domdifsn  9093  domunsncan  9110  omxpenlem  9111  enfixsn  9119  mapdom2  9181  frfi  9290  fofinf1o  9335  finsschain  9362  elfiun  9435  marypha1lem  9438  eqsupd  9462  eqinfd  9491  ordiso2  9522  ordtypelem6  9530  ordtypelem7  9531  ordtypelem10  9534  oismo  9547  wemapsolem  9557  brwdom2  9580  wdomtr  9582  unwdomg  9591  xpwdomg  9592  unxpwdom2  9595  cantnfval2  9683  cantnfle  9685  cantnflem1  9703  cantnf  9707  r1ordg  9798  tcrank  9914  carddomi2  10064  harval2  10091  infxpenlem  10105  infxpenc2lem2  10112  fseqenlem1  10116  dfac8clem  10124  acndom2  10146  infpwfien  10154  iunfictbso  10206  dfac12lem3  10237  infxp  10305  coflim  10352  cofsmo  10360  coftr  10364  sornom  10368  infpssrlem4  10397  enfin2i  10412  fin23lem26  10416  fin23lem27  10419  fin23lem36  10439  fin23lem40  10442  isf32lem5  10448  isf34lem4  10468  isfin1-3  10477  fin1a2lem10  10500  fin1a2lem13  10503  fin1a2s  10505  hsmexlem4  10520  ttukeylem5  10604  ttukeylem6  10605  ttukeylem7  10606  alephval2  10670  gchor  10725  fpwwe2lem6  10734  fpwwe2lem11  10739  fpwwe2  10741  pwfseqlem4a  10759  pwfseqlem4  10760  winalim2  10794  gchina  10797  inar1  10873  nqereq  11033  prlem934  11131  prlem936  11145  addsrmo  11171  mulsrmo  11172  supsrlem  11209  axpre-sup  11267  dedekind  11486  dedekindle  11487  mulge0b  12200  supaddc  12297  supmul1  12299  un0addcl  12652  un0mulcl  12653  uzwo3  13083  qbtwnre  13342  xlemul1a  13431  seqcl2  14176  seqfveq2  14180  seqshft2  14184  monoord  14188  seqsplit  14191  seqf1olem1  14197  seqid2  14204  seqhomo  14205  expnegz  14252  expcan  14325  ltexp2  14326  discr  14397  bcval5  14475  hashbc  14611  hashf1lem2  14614  seqcoll  14622  seqcoll2  14623  wrdind  14885  wrd2ind  14886  sgn3da  15269  cau3lem  15537  ello1d  15705  lo1bdd2  15706  rlimclim  15728  climrlim2  15729  rlimdm  15733  rlimcn1  15770  reccn2  15779  rlimsqzlem  15831  lo1le  15834  caucvgrlem  15855  caurcvg2  15860  summolem2  15897  zsum  15899  fsum  15901  fsumf1o  15904  sumss  15905  fsumss  15906  fsumcl2lem  15912  fsumadd  15921  fsumcom2  15955  fsum0diag2  15964  fsummulc2  15965  fsumconst  15971  fsumrelem  15989  fsumrlim  15993  fsumo1  15994  divrcnv  16036  geomulcvg  16060  mertenslem2  16069  prodmolem2  16117  zprod  16119  fprod  16123  fprodf1o  16128  prodss  16129  fprodss  16130  fprodcl2lem  16132  fprodmul  16142  fproddiv  16143  fprodconst  16160  fprodn0  16161  fprodcom2  16166  ruclem8  16420  dvds0lem  16451  dvdsnegb  16458  dvdssub2  16486  bitsf1  16631  bitsshft  16660  bezoutlem3  16729  bezoutlem4  16730  isprm5  16898  isprm6  16905  hashgcdeq  16982  modprminv  16992  modprminveq  16993  reumodprminv  16997  pcqmul  17046  pcqcl  17049  pcxnn0cl  17053  pcxcl  17054  pc2dvds  17072  pcadd  17082  pcmpt  17085  pockthg  17099  infpnlem1  17103  prmreclem5  17113  vdwlem2  17175  vdwlem9  17182  vdwlem10  17183  vdwlem12  17185  ramub  17206  0ram  17213  ramub1lem2  17220  ramub1  17221  ramcl  17222  mreexexd  17837  acsfn2  17852  iscatd  17862  catpropd  17898  setcmon  18277  pleval2i  18523  psss  18769  mgmidsssn0  18868  mgmhmeql  18920  mhmeql  19037  frmdss2  19074  frmdup3  19078  grprcan  19199  dfgrp3lem  19263  mulgnn0ass  19335  isnsg3  19385  ghmpreima  19467  ghmeql  19468  gaorber  19537  f1omvdco2  19677  psgnunilem1  19722  psgnunilem2  19724  oddvds  19776  gexdvds  19813  sylow1lem1  19827  odcau  19833  pgpssslw  19843  sylow2alem2  19847  sylow2blem3  19851  fislw  19854  lsmmod  19904  efgredlem  19976  frgpup3  20007  gsumval3  20136  gsumzres  20138  gsumzcl2  20139  gsumzf1o  20141  gsumzaddlem  20150  gsumconst  20163  gsumzmhm  20166  gsumzoppg  20173  gsum2d2lem  20202  ablfac1eulem  20303  pgpfac1lem5  20310  ablfaclem3  20318  issubdrg  21052  lss1d  21253  lmhmeql  21345  lspextmo  21346  lspsnat  21438  lsppratlem6  21445  islbs3  21448  lbsextlem4  21454  lidl1el  21520  cnsubrg  21748  gsumfsum  21755  prmirredlem  21793  znidomb  21882  frgpcyg  21894  cssmre  22014  dsmmsubg  22064  dsmmlss  22065  frlmsslsp  22117  lindff1  22141  lindfrn  22142  rnasclassa  22218  mvrf1  22308  mplsubglem  22321  mpllsslem  22322  mplcoe1  22361  mplcoe5  22364  gsummoncoe1  22641  mat1dimcrng  22807  mdetdiaglem  22928  mdetunilem7  22948  mdetunilem8  22949  mdetunilem9  22950  cpmatacl  23049  cpmatmcllem  23051  mp2pm2mplem4  23142  en2top  23318  toponmre  23426  topssnei  23457  innei  23458  clslp  23481  restcls  23514  restntr  23515  ordtrest2lem  23536  cnpco  23600  cncls2  23606  cncnpi  23611  cncnp  23613  cnconst2  23616  cnpdis  23626  lmcnp  23637  cnhaus  23687  isreg2  23710  cncmp  23725  tgcmp  23734  sscmp  23738  cmpfi  23741  cnconn  23755  iunconnlem  23760  clsconn  23763  1stcfb  23778  1stcrest  23786  2ndcctbss  23789  2ndcdisj  23790  1stcelcls  23795  1stccnp  23796  restnlly  23816  cldllycmp  23829  lly1stc  23830  dislly  23831  locfincmp  23860  comppfsc  23866  kgentopon  23872  kgenidm  23881  1stckgenlem  23887  kgencn3  23892  ptpjpre1  23905  ptbasin  23911  txcls  23938  tx2cn  23944  ptpjcn  23945  ptclsg  23949  ptcnp  23956  txdis  23966  txlly  23970  txnlly  23971  pthaus  23972  txtube  23974  txcmplem1  23975  txcmplem2  23976  txcmp  23977  txhaus  23981  txkgen  23986  xkohaus  23987  xkococnlem  23993  xkococn  23994  txconn  24023  qtopeu  24050  qtoprest  24051  regr1lem2  24074  kqreglem1  24075  cmphaushmeo  24134  xkocnv  24148  fgabs  24213  filuni  24219  trufil  24244  ufileu  24253  filufint  24254  fin1aufil  24266  elfm2  24282  rnelfmlem  24286  fmfnfmlem2  24289  fmfnfmlem4  24291  fmufil  24293  flimopn  24309  fbflim2  24311  hausflimi  24314  hausflim  24315  flimcf  24316  flimclslem  24318  flimsncls  24320  hauspwpwf1  24321  cnpflfi  24333  fclsnei  24353  fclscf  24359  flimfnfcls  24362  fclscmp  24364  ufilcmp  24366  fcfnei  24369  cnpfcf  24375  alexsublem  24378  alexsub  24379  alexsubALTlem2  24382  alexsubALTlem3  24383  alexsubALTlem4  24384  ptcmplem3  24388  ptcmplem4  24389  ptcmplem5  24390  symgtgp  24440  tgpconncompeqg  24446  tgpconncomp  24447  ghmcnp  24449  tgpt0  24453  qustgplem  24455  haustsms2  24471  tsmsgsum  24473  tsmsres  24478  tsmsxp  24489  imasdsf1olem  24707  xbln0  24748  blssps  24758  blss  24759  neibl  24835  blcld  24839  metss  24842  metequiv2  24844  met1stc  24855  metrest  24858  prdsxmslem2  24863  metcnp3  24874  nrmmetd  24908  nlmvscnlem1  25020  nrginvrcnlem  25025  nmoleub  25065  icccmplem2  25158  icccmp  25160  reconnlem2  25162  xrge0tsms  25169  metdstri  25186  metdseq0  25189  metdscn  25191  cnmpopc  25264  lebnumlem3  25299  pcoval2  25352  pcopt  25358  nmoleub2lem  25450  nmhmcn  25456  ipcnlem1  25581  cfilfcls  25610  cmetcaulem  25624  iscmet3lem2  25628  iscmet3  25629  equivcau  25636  caubl  25644  bcthlem2  25661  bcthlem3  25662  bcthlem4  25663  bcthlem5  25664  ivthlem2  25788  ivthlem3  25789  ovoliunlem2  25839  ovolicc2lem2  25854  ovolicc2lem5  25857  ovolicc2  25858  ismbl2  25863  nulmbl  25871  nulmbl2  25872  unmbl  25873  shftmbl  25874  voliunlem3  25888  volsup  25892  ioombl1lem4  25897  ioombl1  25898  icombl  25900  ioombl  25901  uniioombl  25925  opnmbllem  25937  volivth  25943  vitali  25949  mbflimsup  26002  i1fadd  26031  itg1addlem4  26035  itg2le  26075  itg2seq  26078  itg2lea  26080  itg2splitlem  26084  itg2split  26085  itg2mono  26089  itg2gt0  26096  itg2cnlem2  26098  itgss  26147  itgfsum  26162  itgcn  26180  ellimc3  26214  limcco  26228  limciun  26229  dvnres  26266  dvnfre  26287  rolle  26325  c1liplem1  26331  dvivth  26345  dvne0  26346  lhop1lem  26348  lhop1  26349  lhop  26351  dvcnvrelem1  26352  dvfsumrlim  26366  dvfsum2  26369  ftc1a  26372  ftc1lem6  26376  itgsubst  26384  tdeglem4  26393  mdegaddle  26407  mdegvscale  26408  mdegmullem  26411  deg1tmle  26451  ply1divex  26470  dvdsq1p  26496  fta1g  26503  fta1b  26505  plyco0  26525  coeeulem  26558  dgrlem  26563  plyco  26575  coemullem  26584  dgreq0  26599  dgrco  26609  plydivex  26633  quotcan  26647  aannenlem1  26670  aalioulem2  26675  aalioulem3  26676  taylthlem1  26715  ulmbdd  26740  itgulm  26750  radcnvlt1  26760  psercnlem1  26767  abelthlem2  26774  abelthlem8  26781  logcnlem5  26989  efopn  27001  cxpmul2z  27034  cxpcn3lem  27090  cxpeq  27100  xrlimcnp  27311  cxplim  27314  o1cxp  27317  cxploglim  27320  scvxcvx  27328  jensen  27331  ftalem1  27415  ftalem2  27416  fta  27422  basellem3  27425  isppw2  27457  ppinprm  27494  chtnprm  27496  mpodvdsmulf1o  27536  dvdsmulf1o  27538  chtublem  27553  perfectlem2  27572  dchrfi  27597  dchrptlem1  27606  dchrptlem2  27607  dchrptlem3  27608  dchrsum2  27610  bposlem1  27626  bposlem3  27628  2sqlem5  27764  2sqlem6  27765  2sqlem8  27768  2sqlem10  27770  2sqb  27774  chebbnd1lem1  27811  chtppilimlem2  27816  dchrisum0flb  27852  dchrisum0fno1  27853  dchrisum0  27862  pntrsumbnd2  27909  pntpbnd1  27928  pntpbnd2  27929  pntlemp  27952  pnt3  27954  qabvle  27967  ostth2lem2  27976  ostth3  27980  ostth  27981  nolt02o  28067  nogt01o  28068  nosupprefixmo  28072  noinfprefixmo  28073  nosupbnd1lem3  28082  nosupbnd1lem4  28083  nosupbnd1lem5  28084  noinfbnd1lem3  28097  noinfbnd1lem4  28098  noinfbnd1lem5  28099  noetasuplem4  28108  noetainflem4  28112  etaslts  28194  cuteq1  28218  madebdaylemlrcut  28300  cutlt  28333  mulsuniflem  28550  bdayons  28677  addonbday  28680  om2noseqlt  28700  n0fincut  28756  bdaypw2n0bndlem  28864  bdayfinbndlem1  28868  z12sge0  28884  readdscl  28900  remulscl  28903  colinearalglem4  29502  axcontlem10  29566  upgrex  29685  smcnlem  31314  ubthlem1  31487  ubthlem3  31489  htthlem  31534  5oalem6  32276  leopmuli  32750  pjnormssi  32785  pjclem4  32816  pj3si  32824  hatomistici  32979  sumdmdlem  33035  wrdt2ind  33572  xrge0tsmsd  33690  isarchiofld  33816  ordtrest2NEWlem  34610  qqhf  34674  eulerpartlemb  35056  ballotlemfc0  35181  ballotlemfcc  35182  soinfdom  35780  subfacp1lem5  36073  erdszelem7  36086  erdszelem11  36090  pconnconn  36120  txpconn  36121  connpconn  36124  sconnpi1  36128  txsconn  36130  cvxsconn  36132  cvmopnlem  36167  cvmfolem  36168  cvmliftmolem2  36171  cvmliftlem7  36180  cvmliftlem10  36183  cvmlift2lem10  36201  cvmlift3lem4  36211  cvmlift3lem8  36215  satfun  36300  msubff1  36445  wzel  36716  wsuclem  36717  btwnouttr2  36917  cgrxfr  36950  btwnxfr  36951  brcolinear  36954  lineext  36971  btwnconn1lem13  36994  midofsegid  36999  segcon2  37000  brsegle  37003  seglecgr12im  37005  segletr  37009  colinbtwnle  37013  broutsideof2  37017  btwnoutside  37020  broutsideof3  37021  outsideoftr  37024  outsideofeq  37025  outsideofeu  37026  outsidele  37027  lineunray  37042  lineelsb2  37043  linethru  37048  nmulrid  37076  nmuladdss  37092  nadddilem1  37099  finminlem  37236  nn0prpwlem  37240  neibastop2lem  37278  neibastop2  37279  neibastop3  37280  topjoin  37283  tailfb  37295  axtcond  37396  relowlssretop  38429  fvineqsneq  38478  wl-sbcom2d-lem1  38634  finixpnum  38671  poimirlem6  38687  poimirlem7  38688  poimirlem13  38694  poimirlem26  38707  poimirlem29  38710  heicant  38716  opnmbllem0  38717  mblfinlem3  38720  ismblfin  38722  ovoliunnfl  38723  voliunnfl  38725  volsupnfl  38726  itg2addnclem  38732  itg2addnclem3  38734  ftc1cnnc  38753  sdclem2  38819  fdc  38822  istotbnd3  38848  isbnd2  38860  isbnd3  38861  prdsbnd  38870  cntotbnd  38873  heibor1lem  38886  heibor1  38887  heiborlem10  38897  rrncmslem  38909  ghomco  38968  1idl  39103  unichnidl  39108  disjlem18  39978  prtlem10  40065  prtlem18  40077  atlatmstc  40519  cvrexchlem  40619  paddasslem14  41033  pexmidlem5N  41174  cdleme29ex  41574  cdlemefr29exN  41602  cdleme32fva  41637  diarnN  42329  dihlsscpre  42434  isnacs3  43864  kelac1  44208  hbtlem5  44273  hbt  44275  dgraa0p  44294  ofoafg  44499  ofoafo  44501  naddcnffo  44509  fzunt  44599  fzuntd  44600  cocanss2  46064  monoordxrv  46633  rlimdmafv  48389  rlimdmafv2  48470  fmtnoprmfac2  48794  perfectALTVlem2  48962  mogoldbb  49025  lindslinindsimp2  49717