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  3197  vtoclgft  3521  moi2  3690  preq12bg  4820  disjxiun  5107  disjxun  5108  wereu2  5638  frpomin  6316  f1ocnv2d  7645  funeldmdif  8030  extmptsuppeq  8170  suppssr  8177  suppssrg  8178  omeulem1  8549  oelim2  8562  oeoa  8564  boxriin  8916  frfi  9239  fipreima  9316  marypha1lem  9391  supiso  9434  ordtypelem10  9487  r1ordg  9738  infxpenc2lem1  9979  acndom  10011  acndom2  10014  cofsmo  10229  cfcoflem  10232  fin23lem28  10300  fin23lem36  10308  isf32lem1  10313  isf32lem2  10314  isf32lem5  10317  isf34lem4  10337  fin1a2lem6  10365  fin1a2s  10374  ttukeylem2  10470  ttukeylem6  10474  fpwwe2lem7  10597  fpwwe2lem11  10601  inar1  10735  grudomon  10777  axpre-sup  11129  un0addcl  12482  un0mulcl  12483  peano2uz2  12629  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  xlemul1a  13255  fzadd2  13527  elfz2nn0  13586  fzind2  13753  expaddz  14078  expmulz  14080  swrdswrd  14677  cau3lem  15328  lo1bdd2  15497  climuni  15525  fsumcom2  15747  fprodcom2  15957  dvdsval2  16232  algcvga  16556  lcmgcdlem  16583  coprmproddvdslem  16639  divgcdcoprmex  16643  iserodd  16813  prmpwdvds  16882  ram0  17000  catpropd  17677  mndind  18762  isgrpinv  18932  gicsubgen  19218  sylow2alem2  19555  sylow2a  19556  frgpuptinv  19708  gsumcom3fi  19916  gsumxp2  19917  ablfac1eu  20012  dvdsrcl2  20282  islss4  20875  ellspsn6  20907  lmhmima  20961  lsmcl  20997  psgnodpm  21504  dsmmlss  21660  islindf4  21754  gsumbagdiag  21847  psrass1lem  21848  coe1tmmul2  22169  dmatscmcl  22397  mdetdiaglem  22492  mdetunilem9  22514  pm2mp  22719  epttop  22903  neindisj  23011  neitr  23074  restcls  23075  restntr  23076  ordtrest2lem  23097  cncnp  23174  cnconst  23178  1stcrest  23347  2ndcdisj  23350  2ndcsep  23353  1stccnp  23356  islly2  23378  1stckgenlem  23447  ptbasin  23471  ptbasfi  23475  ptcnplem  23515  ptcnp  23516  tx1stc  23544  qtophmeo  23711  filconn  23777  filuni  23779  ufileu  23813  elfm3  23844  rnelfmlem  23846  fmfnfmlem4  23851  cnpflf2  23894  alexsubALTlem4  23944  ptcmplem3  23948  ptcmplem4  23949  ptcmplem5  23950  tsmsxplem1  24047  bl2in  24295  metcnpi  24439  metcnpi2  24440  metcnpi3  24441  recld2  24710  icoopnst  24843  iocopnst  24844  ncvs1  25064  iscfil3  25180  iscmet3lem2  25199  ovoliunlem1  25410  ovolicc2lem2  25426  ovolicc2lem4  25428  voliun  25462  volsuplem  25463  dyadmbllem  25507  mbfinf  25573  mbflimsup  25574  itg2seq  25650  itg2splitlem  25656  itg2cnlem1  25669  ellimc3  25787  dvnadd  25838  dvcnvlem  25887  c1liplem1  25908  lhop2  25927  coe1mul3  26011  ply1divex  26049  dvdsq1p  26075  aannenlem1  26243  aalioulem2  26248  dvtaylp  26285  ulmdvlem3  26318  iblulm  26323  cxpmul2z  26607  xrlimcnp  26885  lgambdd  26954  wilthlem2  26986  basellem3  27000  dvdsflsumcom  27105  perfect  27149  dchreq  27176  dchrsum  27187  bposlem1  27202  lgsquad2  27304  dchrisum0fno1  27429  pntibnd  27511  noinfbnd1lem4  27645  cuteq1  27753  madebdaylemlrcut  27817  precsexlem11  28126  recsex  28128  bdayon  28180  noseqp1  28192  noseqrdgfn  28207  remulscllem2  28359  oppperpex  28687  lmieu  28718  ax5seglem5  28867  axeuclid  28897  egrsubgr  29211  nbumgrvtx  29280  wwlksnextsurj  29837  clwwlkccat  29926  numclwwlk2lem1lem  30278  nmcvcn  30631  ubthlem1  30806  leopmul2i  32071  hstel2  32155  atom1d  32289  cdj1i  32369  f1o3d  32558  fsuppcurry1  32655  fsuppcurry2  32656  xrge0addge  32688  isdrng4  33252  prmidl0  33428  mxidlmax  33443  reff  33836  ordtrest2NEWlem  33919  esumcst  34060  eulerpartlemgh  34376  cvmscld  35267  cgrxfr  36050  finminlem  36313  nn0prpwlem  36317  neibastop1  36354  neibastop2lem  36355  tailfb  36372  fvineqsneu  37406  pibt2  37412  finixpnum  37606  lindsenlbs  37616  matunitlindflem2  37618  poimirlem4  37625  poimirlem25  37646  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2addnclem3  37674  ftc1anc  37702  subspopn  37753  prdsbnd  37794  heibor1lem  37810  heiborlem1  37812  heibor  37822  isdrngo2  37959  rngoisocnv  37982  maxidlmax  38044  riotasv3d  38960  lkrpssN  39163  intnatN  39408  elpaddatiN  39806  pexmidlem5N  39975  lhpj1  40023  ltrnu  40122  cdlemn11pre  41211  dihord2pre  41226  dih1dimatlem0  41329  lcfrlem9  41551  remulcand  42434  prjspner1  42621  0prjspnrel  42622  nna4b4nsq  42655  rexrabdioph  42789  ctbnfien  42813  irrapxlem3  42819  elpell14qr2  42857  elpell1qr2  42867  kelac1  43059  iunrelexpuztr  43715  rfovcnvfvd  44003  radcnvrat  44310  nznngen  44312  tz6.12-afv  47178  tz6.12-afv2  47245  iccelpart  47438  prproropf1olem3  47510  lighneallem4  47615  perfectALTV  47728  bgoldbtbndlem3  47812  tgoldbach  47822  grimcnv  47892  grimco  47893  isuspgrim0  47898  grimedg  47939  isubgr3stgrlem7  47975  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  isassintop  48202  ellcoellss  48428  lindslinindsimp2  48456  itscnhlinecirc02plem3  48777  inlinecirc02p  48780  aacllem  49794