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  3212  vtoclgft  3551  moi2  3724  preq12bg  4857  disjxiun  5144  disjxun  5145  wereu2  5685  frpomin  6362  f1ocnv2d  7685  funeldmdif  8071  extmptsuppeq  8211  suppssr  8218  suppssrg  8219  omeulem1  8618  oelim2  8631  oeoa  8633  boxriin  8978  frfi  9318  fipreima  9395  marypha1lem  9470  supiso  9512  ordtypelem10  9564  r1ordg  9815  infxpenc2lem1  10056  acndom  10088  acndom2  10091  cofsmo  10306  cfcoflem  10309  fin23lem28  10377  fin23lem36  10385  isf32lem1  10390  isf32lem2  10391  isf32lem5  10394  isf34lem4  10414  fin1a2lem6  10442  fin1a2s  10451  ttukeylem2  10547  ttukeylem6  10551  fpwwe2lem7  10674  fpwwe2lem11  10678  inar1  10812  grudomon  10854  axpre-sup  11206  un0addcl  12556  un0mulcl  12557  peano2uz2  12703  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  xlemul1a  13326  fzadd2  13595  elfz2nn0  13654  fzind2  13820  expaddz  14143  expmulz  14145  swrdswrd  14739  cau3lem  15389  lo1bdd2  15556  climuni  15584  fsumcom2  15806  fprodcom2  16016  dvdsval2  16289  algcvga  16612  lcmgcdlem  16639  coprmproddvdslem  16695  divgcdcoprmex  16699  iserodd  16868  prmpwdvds  16937  ram0  17055  catpropd  17753  mndind  18853  isgrpinv  19023  gicsubgen  19309  sylow2alem2  19650  sylow2a  19651  frgpuptinv  19803  gsumcom3fi  20011  gsumxp2  20012  ablfac1eu  20107  dvdsrcl2  20382  islss4  20977  ellspsn6  21009  lmhmima  21063  lsmcl  21099  psgnodpm  21623  dsmmlss  21781  islindf4  21875  gsumbagdiag  21968  psrass1lem  21969  coe1tmmul2  22294  dmatscmcl  22524  mdetdiaglem  22619  mdetunilem9  22641  pm2mp  22846  epttop  23031  neindisj  23140  neitr  23203  restcls  23204  restntr  23205  ordtrest2lem  23226  cncnp  23303  cnconst  23307  1stcrest  23476  2ndcdisj  23479  2ndcsep  23482  1stccnp  23485  islly2  23507  1stckgenlem  23576  ptbasin  23600  ptbasfi  23604  ptcnplem  23644  ptcnp  23645  tx1stc  23673  qtophmeo  23840  filconn  23906  filuni  23908  ufileu  23942  elfm3  23973  rnelfmlem  23975  fmfnfmlem4  23980  cnpflf2  24023  alexsubALTlem4  24073  ptcmplem3  24077  ptcmplem4  24078  ptcmplem5  24079  tsmsxplem1  24176  bl2in  24425  metcnpi  24572  metcnpi2  24573  metcnpi3  24574  recld2  24849  icoopnst  24982  iocopnst  24983  ncvs1  25204  iscfil3  25320  iscmet3lem2  25339  ovoliunlem1  25550  ovolicc2lem2  25566  ovolicc2lem4  25568  voliun  25602  volsuplem  25603  dyadmbllem  25647  mbfinf  25713  mbflimsup  25714  itg2seq  25791  itg2splitlem  25797  itg2cnlem1  25810  ellimc3  25928  dvnadd  25979  dvcnvlem  26028  c1liplem1  26049  lhop2  26068  coe1mul3  26152  ply1divex  26190  dvdsq1p  26216  aannenlem1  26384  aalioulem2  26389  dvtaylp  26426  ulmdvlem3  26459  iblulm  26464  cxpmul2z  26747  xrlimcnp  27025  lgambdd  27094  wilthlem2  27126  basellem3  27140  dvdsflsumcom  27245  perfect  27289  dchreq  27316  dchrsum  27327  bposlem1  27342  lgsquad2  27444  dchrisum0fno1  27569  pntibnd  27651  noinfbnd1lem4  27785  cuteq1  27892  madebdaylemlrcut  27951  precsexlem11  28255  recsex  28257  noseqp1  28311  noseqrdgfn  28326  remulscllem2  28447  oppperpex  28775  lmieu  28806  ax5seglem5  28962  axeuclid  28992  egrsubgr  29308  nbumgrvtx  29377  wwlksnextsurj  29929  clwwlkccat  30018  numclwwlk2lem1lem  30370  nmcvcn  30723  ubthlem1  30898  leopmul2i  32163  hstel2  32247  atom1d  32381  cdj1i  32461  f1o3d  32643  fsuppcurry1  32742  fsuppcurry2  32743  xrge0addge  32767  isdrng4  33278  prmidl0  33457  mxidlmax  33472  reff  33799  ordtrest2NEWlem  33882  esumcst  34043  eulerpartlemgh  34359  cvmscld  35257  cgrxfr  36036  finminlem  36300  nn0prpwlem  36304  neibastop1  36341  neibastop2lem  36342  tailfb  36359  fvineqsneu  37393  pibt2  37399  finixpnum  37591  lindsenlbs  37601  matunitlindflem2  37603  poimirlem4  37610  poimirlem25  37631  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  heicant  37641  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2addnclem3  37659  ftc1anc  37687  subspopn  37738  prdsbnd  37779  heibor1lem  37795  heiborlem1  37797  heibor  37807  isdrngo2  37944  rngoisocnv  37967  maxidlmax  38029  riotasv3d  38941  lkrpssN  39144  intnatN  39389  elpaddatiN  39787  pexmidlem5N  39956  lhpj1  40004  ltrnu  40103  cdlemn11pre  41192  dihord2pre  41207  dih1dimatlem0  41310  lcfrlem9  41532  remulcand  42444  prjspner1  42612  0prjspnrel  42613  nna4b4nsq  42646  rexrabdioph  42781  ctbnfien  42805  irrapxlem3  42811  elpell14qr2  42849  elpell1qr2  42859  kelac1  43051  iunrelexpuztr  43708  rfovcnvfvd  43996  radcnvrat  44309  nznngen  44311  tz6.12-afv  47122  tz6.12-afv2  47189  iccelpart  47357  prproropf1olem3  47429  lighneallem4  47534  perfectALTV  47647  bgoldbtbndlem3  47731  tgoldbach  47741  isuspgrim0  47809  uspgrimprop  47810  grimcnv  47816  grimco  47817  grimedg  47840  isubgr3stgrlem7  47874  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  isassintop  48053  ellcoellss  48280  lindslinindsimp2  48308  itscnhlinecirc02plem3  48633  inlinecirc02p  48636  aacllem  49031