Theorem impr 456

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 414	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 420	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  reximddv2  3200  vtoclgft  3499  moi2  3658  preq12bg  4786  disjxiun  5071  disjxun  5072  wereu2  5617  frpomin  6294  f1ocnv2d  7612  funeldmdif  7992  extmptsuppeq  8130  suppssr  8137  suppssrg  8138  omeulem1  8511  oelim2  8525  oeoa  8527  boxriin  8882  frfi  9189  fipreima  9262  marypha1lem  9340  supiso  9383  ordtypelem10  9436  r1ordg  9697  infxpenc2lem1  9936  acndom  9968  acndom2  9971  cofsmo  10187  cfcoflem  10190  fin23lem28  10258  fin23lem36  10266  isf32lem1  10271  isf32lem2  10272  isf32lem5  10275  isf34lem4  10295  fin1a2lem6  10323  fin1a2s  10332  ttukeylem2  10428  ttukeylem6  10432  fpwwe2lem7  10556  fpwwe2lem11  10560  inar1  10694  grudomon  10736  axpre-sup  11088  un0addcl  12465  un0mulcl  12466  peano2uz2  12612  rpnnen1lem2  12922  rpnnen1lem1  12923  rpnnen1lem3  12924  rpnnen1lem5  12926  xlemul1a  13235  fzadd2  13508  elfz2nn0  13567  fzind2  13738  expaddz  14063  expmulz  14065  swrdswrd  14662  cau3lem  15312  lo1bdd2  15481  climuni  15509  fsumcom2  15731  fprodcom2  15944  dvdsval2  16219  algcvga  16543  lcmgcdlem  16570  coprmproddvdslem  16626  divgcdcoprmex  16630  iserodd  16801  prmpwdvds  16870  ram0  16988  catpropd  17670  mndind  18791  isgrpinv  18964  gicsubgen  19248  sylow2alem2  19587  sylow2a  19588  frgpuptinv  19740  gsumcom3fi  19948  gsumxp2  19949  ablfac1eu  20044  dvdsrcl2  20340  islss4  20955  ellspsn6  20987  lmhmima  21040  lsmcl  21076  psgnodpm  21566  dsmmlss  21722  islindf4  21816  gsumbagdiag  21910  psrass1lem  21911  coe1tmmul2  22265  dmatscmcl  22489  mdetdiaglem  22584  mdetunilem9  22606  pm2mp  22811  epttop  22995  neindisj  23103  neitr  23166  restcls  23167  restntr  23168  ordtrest2lem  23189  cncnp  23266  cnconst  23270  1stcrest  23439  2ndcdisj  23442  2ndcsep  23445  1stccnp  23448  islly2  23470  1stckgenlem  23539  ptbasin  23563  ptbasfi  23567  ptcnplem  23607  ptcnp  23608  tx1stc  23636  qtophmeo  23803  filconn  23869  filuni  23871  ufileu  23905  elfm3  23936  rnelfmlem  23938  fmfnfmlem4  23943  cnpflf2  23986  alexsubALTlem4  24036  ptcmplem3  24040  ptcmplem4  24041  ptcmplem5  24042  tsmsxplem1  24139  bl2in  24386  metcnpi  24530  metcnpi2  24531  metcnpi3  24532  recld2  24801  icoopnst  24927  iocopnst  24928  ncvs1  25145  iscfil3  25261  iscmet3lem2  25280  ovoliunlem1  25490  ovolicc2lem2  25506  ovolicc2lem4  25508  voliun  25542  volsuplem  25543  dyadmbllem  25587  mbfinf  25653  mbflimsup  25654  itg2seq  25730  itg2splitlem  25736  itg2cnlem1  25749  ellimc3  25867  dvnadd  25917  dvcnvlem  25964  c1liplem1  25984  lhop2  26003  coe1mul3  26085  ply1divex  26123  dvdsq1p  26149  aannenlem1  26315  aalioulem2  26320  dvtaylp  26356  ulmdvlem3  26388  iblulm  26393  cxpmul2z  26676  xrlimcnp  26953  lgambdd  27021  wilthlem2  27053  basellem3  27067  dvdsflsumcom  27172  perfect  27215  dchreq  27242  dchrsum  27253  bposlem1  27268  lgsquad2  27370  dchrisum0fno1  27495  pntibnd  27577  noinfbnd1lem4  27710  cuteq1  27829  madebdaylemlrcut  27911  precsexlem11  28229  recsex  28231  bdayons  28288  addonbday  28291  noseqp1  28303  noseqrdgfn  28318  bdaypw2n0bndlem  28475  bdayfinbndlem1  28479  remulscllem2  28513  oppperpex  28841  lmieu  28872  ax5seglem5  29022  axeuclid  29052  egrsubgr  29366  nbumgrvtx  29435  wwlksnextsurj  29988  clwwlkccat  30080  numclwwlk2lem1lem  30432  nmcvcn  30786  ubthlem1  30961  leopmul2i  32226  hstel2  32310  atom1d  32444  cdj1i  32524  f1o3d  32720  fsuppcurry1  32818  fsuppcurry2  32819  xrge0addge  32852  isdrng4  33381  prmidl0  33535  mxidlmax  33550  reff  34033  ordtrest2NEWlem  34116  esumcst  34257  eulerpartlemgh  34572  cvmscld  35514  cgrxfr  36296  finminlem  36559  nn0prpwlem  36563  neibastop1  36600  neibastop2lem  36601  tailfb  36618  fvineqsneu  37786  pibt2  37792  finixpnum  37985  lindsenlbs  37995  matunitlindflem2  37997  poimirlem4  38004  poimirlem25  38025  poimirlem26  38026  poimirlem29  38029  poimirlem30  38030  poimirlem31  38031  poimirlem32  38032  heicant  38035  mblfinlem3  38039  mblfinlem4  38040  itg2addnclem  38051  itg2addnclem3  38053  ftc1anc  38081  subspopn  38132  prdsbnd  38173  heibor1lem  38189  heiborlem1  38191  heibor  38201  isdrngo2  38338  rngoisocnv  38361  maxidlmax  38423  riotasv3d  39465  lkrpssN  39668  intnatN  39912  elpaddatiN  40310  pexmidlem5N  40479  lhpj1  40527  ltrnu  40626  cdlemn11pre  41715  dihord2pre  41730  dih1dimatlem0  41833  lcfrlem9  42055  remulcand  42929  prjspner1  43089  0prjspnrel  43090  nna4b4nsq  43123  rexrabdioph  43252  ctbnfien  43276  irrapxlem3  43282  elpell14qr2  43320  elpell1qr2  43330  kelac1  43521  iunrelexpuztr  44176  rfovcnvfvd  44464  radcnvrat  44771  nznngen  44773  tz6.12-afv  47648  tz6.12-afv2  47715  iccelpart  47920  prproropf1olem3  47992  lighneallem4  48100  perfectALTV  48226  bgoldbtbndlem3  48310  tgoldbach  48320  grimcnv  48391  grimco  48392  isuspgrim0  48397  grimedg  48438  isubgr3stgrlem7  48475  gpg5nbgrvtx03starlem1  48571  gpg5nbgrvtx03starlem3  48573  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem3  48576  isassintop  48713  ellcoellss  48938  lindslinindsimp2  48966  itscnhlinecirc02plem3  49287  inlinecirc02p  49290  aacllem  50303