Theorem impr 460

Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
impr.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem impr

Step	Hyp	Ref	Expression
1		impr.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 424	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:  reximddv2  3221  vtoclgft  3515  moi2  3674  preq12bg  4813  disjxiun  5100  disjxun  5101  wereu2  5645  frpomin  6333  f1ocnv2d  7663  funeldmdif  8043  extmptsuppeq  8184  suppssr  8191  suppssrg  8192  omeulem1  8569  oelim2  8583  oeoa  8585  boxriin  8947  frfi  9255  fipreima  9325  marypha1lem  9403  supiso  9446  ordtypelem10  9499  r1ordg  9760  infxpenc2lem1  10055  acndom  10087  acndom2  10090  cofsmo  10304  cfcoflem  10307  fin23lem28  10375  fin23lem36  10383  isf32lem1  10388  isf32lem2  10389  isf32lem5  10392  isf34lem4  10412  fin1a2lem6  10440  fin1a2s  10449  ttukeylem2  10545  ttukeylem6  10549  fpwwe2lem7  10679  fpwwe2lem11  10683  inar1  10817  grudomon  10859  axpre-sup  11211  un0addcl  12594  un0mulcl  12595  peano2uz2  12742  rpnnen1lem2  13060  rpnnen1lem1  13061  rpnnen1lem3  13062  rpnnen1lem5  13064  xlemul1a  13373  fzadd2  13647  elfz2nn0  13706  fzind2  13877  expaddz  14203  expmulz  14205  swrdswrd  14807  cau3lem  15475  lo1bdd2  15644  climuni  15672  fsumcom2  15893  fprodcom2  16104  dvdsval2  16378  algcvga  16702  lcmgcdlem  16729  coprmproddvdslem  16785  divgcdcoprmex  16789  iserodd  16960  prmpwdvds  17029  ram0  17147  catpropd  17830  mndind  18971  isgrpinv  19151  gicsubgen  19440  sylow2alem2  19779  sylow2a  19780  frgpuptinv  19932  gsumcom3fi  20140  gsumxp2  20141  ablfac1eu  20236  dvdsrcl2  20543  isdrng4  20939  isdrng3lem2  20953  islss4  21184  ellspsn6  21216  lmhmima  21269  lsmcl  21305  prmidl0  21581  psgnodpm  21841  dsmmlss  21997  islindf4  22091  lindsenlbs  22104  gsumbagdiag  22187  psrass1lem  22188  coe1tmmul2  22542  dmatscmcl  22765  mdetdiaglem  22860  mdetunilem9  22882  matunitlindflem2  22942  pm2mp  23090  epttop  23274  neindisj  23382  neitr  23445  restcls  23446  restntr  23447  ordtrest2lem  23468  cncnp  23545  cnconst  23549  1stcrest  23718  2ndcdisj  23722  2ndcsep  23725  1stccnp  23728  islly2  23750  1stckgenlem  23819  ptbasin  23843  ptbasfi  23847  ptcnplem  23887  ptcnp  23888  tx1stc  23916  qtophmeo  24083  filconn  24149  filuni  24151  ufileu  24185  elfm3  24216  rnelfmlem  24218  fmfnfmlem4  24223  cnpflf2  24266  alexsubALTlem4  24316  ptcmplem3  24320  ptcmplem4  24321  ptcmplem5  24322  tsmsxplem1  24419  bl2in  24666  metcnpi  24810  metcnpi2  24811  metcnpi3  24812  recld2  25081  icoopnst  25207  iocopnst  25208  ncvs1  25425  iscfil3  25541  iscmet3lem2  25560  ovoliunlem1  25770  ovolicc2lem2  25786  ovolicc2lem4  25788  voliun  25822  volsuplem  25823  dyadmbllem  25867  mbfinf  25933  mbflimsup  25934  itg2seq  26010  itg2splitlem  26016  itg2cnlem1  26029  ellimc3  26146  dvnadd  26196  dvcnvlem  26243  c1liplem1  26263  lhop2  26282  coe1mul3  26364  ply1divex  26402  dvdsq1p  26428  preimaaa  26595  aannenlem1  26604  aalioulem2  26609  dvtaylp  26646  ulmdvlem3  26678  iblulm  26683  cxpmul2z  26968  xrlimcnp  27245  lgambdd  27313  wilthlem2  27345  basellem3  27359  dvdsflsumcom  27464  perfect  27507  dchreq  27534  dchrsum  27545  bposlem1  27560  lgsquad2  27662  dchrisum0fno1  27787  pntibnd  27869  noinfbnd1lem4  28002  cuteq1  28122  madebdaylemlrcut  28204  precsexlem11  28522  recsex  28524  bdayons  28581  addonbday  28584  noseqp1  28596  noseqrdgfn  28611  bdaypw2n0bndlem  28768  bdayfinbndlem1  28772  remulscllem2  28806  oppperpex  29148  lmieu  29208  ax5seglem5  29430  axeuclid  29460  egrsubgr  29777  nbumgrvtx  29846  wwlksnextsurj  30408  clwwlkccat  30500  numclwwlk2lem1lem  30862  nmcvcn  31216  ubthlem1  31391  leopmul2i  32656  hstel2  32740  atom1d  32874  cdj1i  32954  f1o3d  33139  fsuppcurry1  33235  fsuppcurry2  33236  xrge0addge  33269  mxidlmax  33909  reff  34390  ordtrest2NEWlem  34473  esumcst  34614  eulerpartlemgh  34930  cvmscld  35953  cgrxfr  36736  finminlem  37022  nn0prpwlem  37026  neibastop1  37063  neibastop2lem  37064  tailfb  37081  fvineqsneu  38248  pibt2  38254  finixpnum  38442  poimirlem4  38456  poimirlem25  38477  poimirlem26  38478  poimirlem29  38481  poimirlem30  38482  poimirlem31  38483  poimirlem32  38484  heicant  38487  mblfinlem3  38491  mblfinlem4  38492  itg2addnclem  38503  itg2addnclem3  38505  ftc1anc  38533  subspopn  38600  prdsbnd  38641  heibor1lem  38657  heiborlem1  38659  heibor  38669  isdrngo2  38806  rngoisocnv  38829  maxidlmax  38891  riotasv3d  39931  lkrpssN  40134  intnatN  40378  elpaddatiN  40776  pexmidlem5N  40945  lhpj1  40993  ltrnu  41092  cdlemn11pre  42181  dihord2pre  42196  dih1dimatlem0  42299  lcfrlem9  42521  remulcand  43412  prjspner1  43570  0prjspnrel  43571  nna4b4nsq  43604  rexrabdioph  43733  ctbnfien  43757  irrapxlem3  43763  elpell14qr2  43801  elpell1qr2  43811  kelac1  44002  iunrelexpuztr  44657  rfovcnvfvd  44945  radcnvrat  45236  nznngen  45238  tz6.12-afv  48159  tz6.12-afv2  48226  iccelpart  48431  prproropf1olem3  48503  lighneallem4  48611  perfectALTV  48737  bgoldbtbndlem3  48821  tgoldbach  48831  grimcnv  48902  grimco  48903  isuspgrim0  48908  grimedg  48949  isubgr3stgrlem7  48986  gpg5nbgrvtx03starlem1  49082  gpg5nbgrvtx03starlem3  49084  gpg5nbgrvtx13starlem1  49085  gpg5nbgrvtx13starlem3  49087  isassintop  49223  ellcoellss  49463  lindslinindsimp2  49491  itscnhlinecirc02plem3  49812  inlinecirc02p  49815  aacllem  50855