Theorem impr 459

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reximddv2  3222  vtoclgft  3519  moi2  3678  preq12bg  4817  disjxiun  5105  disjxun  5106  wereu2  5658  frpomin  6341  f1ocnv2d  7663  funeldmdif  8044  extmptsuppeq  8183  suppssr  8190  suppssrg  8191  omeulem1  8566  oelim2  8580  oeoa  8582  boxriin  8937  frfi  9244  fipreima  9314  marypha1lem  9392  supiso  9435  ordtypelem10  9488  r1ordg  9749  infxpenc2lem1  10002  acndom  10034  acndom2  10037  cofsmo  10252  cfcoflem  10255  fin23lem28  10323  fin23lem36  10331  isf32lem1  10336  isf32lem2  10337  isf32lem5  10340  isf34lem4  10360  fin1a2lem6  10388  fin1a2s  10397  ttukeylem2  10493  ttukeylem6  10497  fpwwe2lem7  10621  fpwwe2lem11  10625  inar1  10759  grudomon  10801  axpre-sup  11153  un0addcl  12536  un0mulcl  12537  peano2uz2  12683  rpnnen1lem2  13000  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem5  13004  xlemul1a  13313  fzadd2  13586  elfz2nn0  13645  fzind2  13816  expaddz  14141  expmulz  14143  swrdswrd  14741  cau3lem  15405  lo1bdd2  15574  climuni  15602  fsumcom2  15824  fprodcom2  16037  dvdsval2  16312  algcvga  16636  lcmgcdlem  16663  coprmproddvdslem  16719  divgcdcoprmex  16723  iserodd  16894  prmpwdvds  16963  ram0  17081  catpropd  17764  mndind  18886  isgrpinv  19059  gicsubgen  19348  sylow2alem2  19687  sylow2a  19688  frgpuptinv  19840  gsumcom3fi  20048  gsumxp2  20049  ablfac1eu  20144  dvdsrcl2  20447  isdrng4  20824  islss4  21062  ellspsn6  21094  lmhmima  21147  lsmcl  21183  prmidl0  21457  psgnodpm  21717  dsmmlss  21873  islindf4  21967  gsumbagdiag  22061  psrass1lem  22062  coe1tmmul2  22416  dmatscmcl  22639  mdetdiaglem  22734  mdetunilem9  22756  pm2mp  22961  epttop  23145  neindisj  23253  neitr  23316  restcls  23317  restntr  23318  ordtrest2lem  23339  cncnp  23416  cnconst  23420  1stcrest  23589  2ndcdisj  23592  2ndcsep  23595  1stccnp  23598  islly2  23620  1stckgenlem  23689  ptbasin  23713  ptbasfi  23717  ptcnplem  23757  ptcnp  23758  tx1stc  23786  qtophmeo  23953  filconn  24019  filuni  24021  ufileu  24055  elfm3  24086  rnelfmlem  24088  fmfnfmlem4  24093  cnpflf2  24136  alexsubALTlem4  24186  ptcmplem3  24190  ptcmplem4  24191  ptcmplem5  24192  tsmsxplem1  24289  bl2in  24536  metcnpi  24680  metcnpi2  24681  metcnpi3  24682  recld2  24951  icoopnst  25077  iocopnst  25078  ncvs1  25295  iscfil3  25411  iscmet3lem2  25430  ovoliunlem1  25640  ovolicc2lem2  25656  ovolicc2lem4  25658  voliun  25692  volsuplem  25693  dyadmbllem  25737  mbfinf  25803  mbflimsup  25804  itg2seq  25880  itg2splitlem  25886  itg2cnlem1  25899  ellimc3  26017  dvnadd  26067  dvcnvlem  26114  c1liplem1  26134  lhop2  26153  coe1mul3  26235  ply1divex  26273  dvdsq1p  26299  aannenlem1  26468  aalioulem2  26473  dvtaylp  26509  ulmdvlem3  26541  iblulm  26546  cxpmul2z  26832  xrlimcnp  27109  lgambdd  27177  wilthlem2  27209  basellem3  27223  dvdsflsumcom  27328  perfect  27371  dchreq  27398  dchrsum  27409  bposlem1  27424  lgsquad2  27526  dchrisum0fno1  27651  pntibnd  27733  noinfbnd1lem4  27866  cuteq1  27986  madebdaylemlrcut  28068  precsexlem11  28386  recsex  28388  bdayons  28445  addonbday  28448  noseqp1  28460  noseqrdgfn  28475  bdaypw2n0bndlem  28632  bdayfinbndlem1  28636  remulscllem2  28670  oppperpex  29009  lmieu  29067  ax5seglem5  29249  axeuclid  29279  egrsubgr  29593  nbumgrvtx  29662  wwlksnextsurj  30215  clwwlkccat  30307  numclwwlk2lem1lem  30659  nmcvcn  31013  ubthlem1  31188  leopmul2i  32453  hstel2  32537  atom1d  32671  cdj1i  32751  f1o3d  32937  fsuppcurry1  33035  fsuppcurry2  33036  xrge0addge  33069  mxidlmax  33714  reff  34195  ordtrest2NEWlem  34278  esumcst  34419  eulerpartlemgh  34734  cvmscld  35719  cgrxfr  36501  finminlem  36773  nn0prpwlem  36777  neibastop1  36814  neibastop2lem  36815  tailfb  36832  fvineqsneu  38001  pibt2  38007  finixpnum  38200  lindsenlbs  38210  matunitlindflem2  38212  poimirlem4  38219  poimirlem25  38240  poimirlem26  38241  poimirlem29  38244  poimirlem30  38245  poimirlem31  38246  poimirlem32  38247  heicant  38250  mblfinlem3  38254  mblfinlem4  38255  itg2addnclem  38266  itg2addnclem3  38268  ftc1anc  38296  subspopn  38347  prdsbnd  38388  heibor1lem  38404  heiborlem1  38406  heibor  38416  isdrngo2  38553  rngoisocnv  38576  maxidlmax  38638  riotasv3d  39680  lkrpssN  39883  intnatN  40127  elpaddatiN  40525  pexmidlem5N  40694  lhpj1  40742  ltrnu  40841  cdlemn11pre  41930  dihord2pre  41945  dih1dimatlem0  42048  lcfrlem9  42270  remulcand  43146  prjspner1  43306  0prjspnrel  43307  nna4b4nsq  43340  rexrabdioph  43469  ctbnfien  43493  irrapxlem3  43499  elpell14qr2  43537  elpell1qr2  43547  kelac1  43738  iunrelexpuztr  44393  rfovcnvfvd  44681  radcnvrat  44972  nznngen  44974  tz6.12-afv  47855  tz6.12-afv2  47922  iccelpart  48127  prproropf1olem3  48199  lighneallem4  48307  perfectALTV  48433  bgoldbtbndlem3  48517  tgoldbach  48527  grimcnv  48598  grimco  48599  isuspgrim0  48604  grimedg  48645  isubgr3stgrlem7  48682  gpg5nbgrvtx03starlem1  48778  gpg5nbgrvtx03starlem3  48780  gpg5nbgrvtx13starlem1  48781  gpg5nbgrvtx13starlem3  48783  isassintop  48920  ellcoellss  49160  lindslinindsimp2  49188  itscnhlinecirc02plem3  49509  inlinecirc02p  49512  aacllem  50546