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  3200  vtoclgft  3531  moi2  3699  preq12bg  4829  disjxiun  5116  disjxun  5117  wereu2  5651  frpomin  6329  f1ocnv2d  7658  funeldmdif  8045  extmptsuppeq  8185  suppssr  8192  suppssrg  8193  omeulem1  8592  oelim2  8605  oeoa  8607  boxriin  8952  frfi  9291  fipreima  9368  marypha1lem  9443  supiso  9486  ordtypelem10  9539  r1ordg  9790  infxpenc2lem1  10031  acndom  10063  acndom2  10066  cofsmo  10281  cfcoflem  10284  fin23lem28  10352  fin23lem36  10360  isf32lem1  10365  isf32lem2  10366  isf32lem5  10369  isf34lem4  10389  fin1a2lem6  10417  fin1a2s  10426  ttukeylem2  10522  ttukeylem6  10526  fpwwe2lem7  10649  fpwwe2lem11  10653  inar1  10787  grudomon  10829  axpre-sup  11181  un0addcl  12532  un0mulcl  12533  peano2uz2  12679  rpnnen1lem2  12991  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  xlemul1a  13302  fzadd2  13574  elfz2nn0  13633  fzind2  13799  expaddz  14122  expmulz  14124  swrdswrd  14721  cau3lem  15371  lo1bdd2  15538  climuni  15566  fsumcom2  15788  fprodcom2  15998  dvdsval2  16273  algcvga  16596  lcmgcdlem  16623  coprmproddvdslem  16679  divgcdcoprmex  16683  iserodd  16853  prmpwdvds  16922  ram0  17040  catpropd  17719  mndind  18804  isgrpinv  18974  gicsubgen  19260  sylow2alem2  19597  sylow2a  19598  frgpuptinv  19750  gsumcom3fi  19958  gsumxp2  19959  ablfac1eu  20054  dvdsrcl2  20324  islss4  20917  ellspsn6  20949  lmhmima  21003  lsmcl  21039  psgnodpm  21546  dsmmlss  21702  islindf4  21796  gsumbagdiag  21889  psrass1lem  21890  coe1tmmul2  22211  dmatscmcl  22439  mdetdiaglem  22534  mdetunilem9  22556  pm2mp  22761  epttop  22945  neindisj  23053  neitr  23116  restcls  23117  restntr  23118  ordtrest2lem  23139  cncnp  23216  cnconst  23220  1stcrest  23389  2ndcdisj  23392  2ndcsep  23395  1stccnp  23398  islly2  23420  1stckgenlem  23489  ptbasin  23513  ptbasfi  23517  ptcnplem  23557  ptcnp  23558  tx1stc  23586  qtophmeo  23753  filconn  23819  filuni  23821  ufileu  23855  elfm3  23886  rnelfmlem  23888  fmfnfmlem4  23893  cnpflf2  23936  alexsubALTlem4  23986  ptcmplem3  23990  ptcmplem4  23991  ptcmplem5  23992  tsmsxplem1  24089  bl2in  24337  metcnpi  24481  metcnpi2  24482  metcnpi3  24483  recld2  24752  icoopnst  24885  iocopnst  24886  ncvs1  25107  iscfil3  25223  iscmet3lem2  25242  ovoliunlem1  25453  ovolicc2lem2  25469  ovolicc2lem4  25471  voliun  25505  volsuplem  25506  dyadmbllem  25550  mbfinf  25616  mbflimsup  25617  itg2seq  25693  itg2splitlem  25699  itg2cnlem1  25712  ellimc3  25830  dvnadd  25881  dvcnvlem  25930  c1liplem1  25951  lhop2  25970  coe1mul3  26054  ply1divex  26092  dvdsq1p  26118  aannenlem1  26286  aalioulem2  26291  dvtaylp  26328  ulmdvlem3  26361  iblulm  26366  cxpmul2z  26650  xrlimcnp  26928  lgambdd  26997  wilthlem2  27029  basellem3  27043  dvdsflsumcom  27148  perfect  27192  dchreq  27219  dchrsum  27230  bposlem1  27245  lgsquad2  27347  dchrisum0fno1  27472  pntibnd  27554  noinfbnd1lem4  27688  cuteq1  27795  madebdaylemlrcut  27854  precsexlem11  28158  recsex  28160  noseqp1  28214  noseqrdgfn  28229  remulscllem2  28350  oppperpex  28678  lmieu  28709  ax5seglem5  28858  axeuclid  28888  egrsubgr  29202  nbumgrvtx  29271  wwlksnextsurj  29828  clwwlkccat  29917  numclwwlk2lem1lem  30269  nmcvcn  30622  ubthlem1  30797  leopmul2i  32062  hstel2  32146  atom1d  32280  cdj1i  32360  f1o3d  32551  fsuppcurry1  32648  fsuppcurry2  32649  xrge0addge  32681  isdrng4  33235  prmidl0  33411  mxidlmax  33426  reff  33816  ordtrest2NEWlem  33899  esumcst  34040  eulerpartlemgh  34356  cvmscld  35241  cgrxfr  36019  finminlem  36282  nn0prpwlem  36286  neibastop1  36323  neibastop2lem  36324  tailfb  36341  fvineqsneu  37375  pibt2  37381  finixpnum  37575  lindsenlbs  37585  matunitlindflem2  37587  poimirlem4  37594  poimirlem25  37615  poimirlem26  37616  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  heicant  37625  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2addnclem3  37643  ftc1anc  37671  subspopn  37722  prdsbnd  37763  heibor1lem  37779  heiborlem1  37781  heibor  37791  isdrngo2  37928  rngoisocnv  37951  maxidlmax  38013  riotasv3d  38924  lkrpssN  39127  intnatN  39372  elpaddatiN  39770  pexmidlem5N  39939  lhpj1  39987  ltrnu  40086  cdlemn11pre  41175  dihord2pre  41190  dih1dimatlem0  41293  lcfrlem9  41515  remulcand  42428  prjspner1  42596  0prjspnrel  42597  nna4b4nsq  42630  rexrabdioph  42764  ctbnfien  42788  irrapxlem3  42794  elpell14qr2  42832  elpell1qr2  42842  kelac1  43034  iunrelexpuztr  43690  rfovcnvfvd  43978  radcnvrat  44286  nznngen  44288  tz6.12-afv  47150  tz6.12-afv2  47217  iccelpart  47395  prproropf1olem3  47467  lighneallem4  47572  perfectALTV  47685  bgoldbtbndlem3  47769  tgoldbach  47779  grimcnv  47849  grimco  47850  isuspgrim0  47855  grimedg  47896  isubgr3stgrlem7  47932  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem3  48023  isassintop  48133  ellcoellss  48359  lindslinindsimp2  48387  itscnhlinecirc02plem3  48712  inlinecirc02p  48715  aacllem  49613