Theorem impr 454

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 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	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:  reximddv2  3197  vtoclgft  3498  moi2  3663  preq12bg  4797  disjxiun  5083  disjxun  5084  wereu2  5619  frpomin  6296  f1ocnv2d  7611  funeldmdif  7992  extmptsuppeq  8129  suppssr  8136  suppssrg  8137  omeulem1  8508  oelim2  8522  oeoa  8524  boxriin  8879  frfi  9186  fipreima  9259  marypha1lem  9337  supiso  9380  ordtypelem10  9433  r1ordg  9691  infxpenc2lem1  9930  acndom  9962  acndom2  9965  cofsmo  10180  cfcoflem  10183  fin23lem28  10251  fin23lem36  10259  isf32lem1  10264  isf32lem2  10265  isf32lem5  10268  isf34lem4  10288  fin1a2lem6  10316  fin1a2s  10325  ttukeylem2  10421  ttukeylem6  10425  fpwwe2lem7  10549  fpwwe2lem11  10553  inar1  10687  grudomon  10729  axpre-sup  11081  un0addcl  12459  un0mulcl  12460  peano2uz2  12606  rpnnen1lem2  12916  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem5  12920  xlemul1a  13229  fzadd2  13502  elfz2nn0  13561  fzind2  13732  expaddz  14057  expmulz  14059  swrdswrd  14656  cau3lem  15306  lo1bdd2  15475  climuni  15503  fsumcom2  15725  fprodcom2  15938  dvdsval2  16213  algcvga  16537  lcmgcdlem  16564  coprmproddvdslem  16620  divgcdcoprmex  16624  iserodd  16795  prmpwdvds  16864  ram0  16982  catpropd  17664  mndind  18785  isgrpinv  18958  gicsubgen  19243  sylow2alem2  19582  sylow2a  19583  frgpuptinv  19735  gsumcom3fi  19943  gsumxp2  19944  ablfac1eu  20039  dvdsrcl2  20335  islss4  20946  ellspsn6  20978  lmhmima  21032  lsmcl  21068  psgnodpm  21576  dsmmlss  21732  islindf4  21826  gsumbagdiag  21919  psrass1lem  21920  coe1tmmul2  22250  dmatscmcl  22477  mdetdiaglem  22572  mdetunilem9  22594  pm2mp  22799  epttop  22983  neindisj  23091  neitr  23154  restcls  23155  restntr  23156  ordtrest2lem  23177  cncnp  23254  cnconst  23258  1stcrest  23427  2ndcdisj  23430  2ndcsep  23433  1stccnp  23436  islly2  23458  1stckgenlem  23527  ptbasin  23551  ptbasfi  23555  ptcnplem  23595  ptcnp  23596  tx1stc  23624  qtophmeo  23791  filconn  23857  filuni  23859  ufileu  23893  elfm3  23924  rnelfmlem  23926  fmfnfmlem4  23931  cnpflf2  23974  alexsubALTlem4  24024  ptcmplem3  24028  ptcmplem4  24029  ptcmplem5  24030  tsmsxplem1  24127  bl2in  24374  metcnpi  24518  metcnpi2  24519  metcnpi3  24520  recld2  24789  icoopnst  24915  iocopnst  24916  ncvs1  25133  iscfil3  25249  iscmet3lem2  25268  ovoliunlem1  25478  ovolicc2lem2  25494  ovolicc2lem4  25496  voliun  25530  volsuplem  25531  dyadmbllem  25575  mbfinf  25641  mbflimsup  25642  itg2seq  25718  itg2splitlem  25724  itg2cnlem1  25737  ellimc3  25855  dvnadd  25905  dvcnvlem  25952  c1liplem1  25973  lhop2  25992  coe1mul3  26076  ply1divex  26114  dvdsq1p  26140  aannenlem1  26307  aalioulem2  26312  dvtaylp  26349  ulmdvlem3  26382  iblulm  26387  cxpmul2z  26671  xrlimcnp  26949  lgambdd  27018  wilthlem2  27050  basellem3  27064  dvdsflsumcom  27169  perfect  27213  dchreq  27240  dchrsum  27251  bposlem1  27266  lgsquad2  27368  dchrisum0fno1  27493  pntibnd  27575  noinfbnd1lem4  27709  cuteq1  27828  madebdaylemlrcut  27910  precsexlem11  28228  recsex  28230  bdayons  28287  addonbday  28290  noseqp1  28302  noseqrdgfn  28317  bdaypw2n0bndlem  28474  bdayfinbndlem1  28478  remulscllem2  28512  oppperpex  28840  lmieu  28871  ax5seglem5  29021  axeuclid  29051  egrsubgr  29365  nbumgrvtx  29434  wwlksnextsurj  29988  clwwlkccat  30080  numclwwlk2lem1lem  30432  nmcvcn  30786  ubthlem1  30961  leopmul2i  32226  hstel2  32310  atom1d  32444  cdj1i  32524  f1o3d  32719  fsuppcurry1  32817  fsuppcurry2  32818  xrge0addge  32851  isdrng4  33376  prmidl0  33530  mxidlmax  33545  reff  34004  ordtrest2NEWlem  34087  esumcst  34228  eulerpartlemgh  34543  cvmscld  35476  cgrxfr  36258  finminlem  36521  nn0prpwlem  36525  neibastop1  36562  neibastop2lem  36563  tailfb  36580  fvineqsneu  37738  pibt2  37744  finixpnum  37937  lindsenlbs  37947  matunitlindflem2  37949  poimirlem4  37956  poimirlem25  37977  poimirlem26  37978  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimirlem32  37984  heicant  37987  mblfinlem3  37991  mblfinlem4  37992  itg2addnclem  38003  itg2addnclem3  38005  ftc1anc  38033  subspopn  38084  prdsbnd  38125  heibor1lem  38141  heiborlem1  38143  heibor  38153  isdrngo2  38290  rngoisocnv  38313  maxidlmax  38375  riotasv3d  39417  lkrpssN  39620  intnatN  39864  elpaddatiN  40262  pexmidlem5N  40431  lhpj1  40479  ltrnu  40578  cdlemn11pre  41667  dihord2pre  41682  dih1dimatlem0  41785  lcfrlem9  42007  remulcand  42882  prjspner1  43070  0prjspnrel  43071  nna4b4nsq  43104  rexrabdioph  43237  ctbnfien  43261  irrapxlem3  43267  elpell14qr2  43305  elpell1qr2  43315  kelac1  43506  iunrelexpuztr  44161  rfovcnvfvd  44449  radcnvrat  44756  nznngen  44758  tz6.12-afv  47618  tz6.12-afv2  47685  iccelpart  47890  prproropf1olem3  47962  lighneallem4  48070  perfectALTV  48196  bgoldbtbndlem3  48280  tgoldbach  48290  grimcnv  48361  grimco  48362  isuspgrim0  48367  grimedg  48408  isubgr3stgrlem7  48445  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem3  48546  isassintop  48683  ellcoellss  48908  lindslinindsimp2  48936  itscnhlinecirc02plem3  49257  inlinecirc02p  49260  aacllem  50273