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 206  df-an 396

This theorem is referenced by:  reximddv2  3206  moi2  3646  preq12bg  4781  disjxiun  5067  disjxun  5068  wereu2  5577  frpomin  6228  f1ocnv2d  7500  funeldmdif  7862  extmptsuppeq  7975  suppssr  7983  suppssrg  7984  omeulem1  8375  oelim2  8388  oeoa  8390  boxriin  8686  frfi  8989  fipreima  9055  marypha1lem  9122  supiso  9164  ordtypelem10  9216  r1ordg  9467  infxpenc2lem1  9706  acndom  9738  acndom2  9741  cofsmo  9956  cfcoflem  9959  fin23lem28  10027  fin23lem36  10035  isf32lem1  10040  isf32lem2  10041  isf32lem5  10044  isf34lem4  10064  fin1a2lem6  10092  fin1a2s  10101  ttukeylem2  10197  ttukeylem6  10201  fpwwe2lem7  10324  fpwwe2lem11  10328  inar1  10462  grudomon  10504  axpre-sup  10856  un0addcl  12196  un0mulcl  12197  peano2uz2  12338  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  xlemul1a  12951  fzadd2  13220  elfz2nn0  13276  fzind2  13433  expaddz  13755  expmulz  13757  swrdswrd  14346  cau3lem  14994  lo1bdd2  15161  climuni  15189  fsumcom2  15414  fprodcom2  15622  dvdsval2  15894  algcvga  16212  lcmgcdlem  16239  coprmproddvdslem  16295  divgcdcoprmex  16299  iserodd  16464  prmpwdvds  16533  ram0  16651  catpropd  17335  mndind  18381  isgrpinv  18547  gicsubgen  18809  sylow2alem2  19138  sylow2a  19139  frgpuptinv  19292  gsumcom3fi  19495  gsumxp2  19496  ablfac1eu  19591  dvdsrcl2  19807  islss4  20139  lspsnel6  20171  lmhmima  20224  lsmcl  20260  psgnodpm  20705  dsmmlss  20861  islindf4  20955  gsumbagdiagOLD  21052  psrass1lemOLD  21053  gsumbagdiag  21055  psrass1lem  21056  coe1tmmul2  21357  dmatscmcl  21560  mdetdiaglem  21655  mdetunilem9  21677  pm2mp  21882  epttop  22067  neindisj  22176  neitr  22239  restcls  22240  restntr  22241  ordtrest2lem  22262  cncnp  22339  cnconst  22343  1stcrest  22512  2ndcdisj  22515  2ndcsep  22518  1stccnp  22521  islly2  22543  1stckgenlem  22612  ptbasin  22636  ptbasfi  22640  ptcnplem  22680  ptcnp  22681  tx1stc  22709  qtophmeo  22876  filconn  22942  filuni  22944  ufileu  22978  elfm3  23009  rnelfmlem  23011  fmfnfmlem4  23016  cnpflf2  23059  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem4  23114  ptcmplem5  23115  tsmsxplem1  23212  bl2in  23461  metcnpi  23606  metcnpi2  23607  metcnpi3  23608  recld2  23883  icoopnst  24008  iocopnst  24009  ncvs1  24226  iscfil3  24342  iscmet3lem2  24361  ovoliunlem1  24571  ovolicc2lem2  24587  ovolicc2lem4  24589  voliun  24623  volsuplem  24624  dyadmbllem  24668  mbfinf  24734  mbflimsup  24735  itg2seq  24812  itg2splitlem  24818  itg2cnlem1  24831  ellimc3  24948  dvnadd  24998  dvcnvlem  25045  c1liplem1  25065  lhop2  25084  coe1mul3  25169  ply1divex  25206  dvdsq1p  25230  aannenlem1  25393  aalioulem2  25398  dvtaylp  25434  ulmdvlem3  25466  iblulm  25471  cxpmul2z  25751  xrlimcnp  26023  lgambdd  26091  wilthlem2  26123  basellem3  26137  dvdsflsumcom  26242  perfect  26284  dchreq  26311  dchrsum  26322  bposlem1  26337  lgsquad2  26439  dchrisum0fno1  26564  pntibnd  26646  oppperpex  27018  lmieu  27049  ax5seglem5  27204  axeuclid  27234  egrsubgr  27547  nbumgrvtx  27616  wwlksnextsurj  28166  clwwlkccat  28255  numclwwlk2lem1lem  28607  nmcvcn  28958  ubthlem1  29133  leopmul2i  30398  hstel2  30482  atom1d  30616  cdj1i  30696  f1o3d  30863  fsuppcurry1  30962  fsuppcurry2  30963  xrge0addge  30982  prmidl0  31528  mxidlmax  31539  reff  31691  ordtrest2NEWlem  31774  esumcst  31931  eulerpartlemgh  32245  cvmscld  33135  noinfbnd1lem4  33856  madebdaylemlrcut  34006  cgrxfr  34284  finminlem  34434  nn0prpwlem  34438  neibastop1  34475  neibastop2lem  34476  tailfb  34493  fvineqsneu  35509  pibt2  35515  finixpnum  35689  lindsenlbs  35699  matunitlindflem2  35701  poimirlem4  35708  poimirlem25  35729  poimirlem26  35730  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  heicant  35739  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  itg2addnclem3  35757  ftc1anc  35785  subspopn  35837  prdsbnd  35878  heibor1lem  35894  heiborlem1  35896  heibor  35906  isdrngo2  36043  rngoisocnv  36066  maxidlmax  36128  riotasv3d  36901  lkrpssN  37104  intnatN  37348  elpaddatiN  37746  pexmidlem5N  37915  lhpj1  37963  ltrnu  38062  cdlemn11pre  39151  dihord2pre  39166  dih1dimatlem0  39269  lcfrlem9  39491  remulcand  40341  prjspner1  40384  0prjspnrel  40385  nna4b4nsq  40413  rexrabdioph  40532  ctbnfien  40556  irrapxlem3  40562  elpell14qr2  40600  elpell1qr2  40610  kelac1  40804  iunrelexpuztr  41216  rfovcnvfvd  41504  radcnvrat  41821  nznngen  41823  tz6.12-afv  44552  tz6.12-afv2  44619  iccelpart  44773  prproropf1olem3  44845  lighneallem4  44950  perfectALTV  45063  bgoldbtbndlem3  45147  tgoldbach  45157  isomuspgr  45174  isassintop  45292  ellcoellss  45664  lindslinindsimp2  45692  itscnhlinecirc02plem3  46018  inlinecirc02p  46021  aacllem  46391