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  3221  vtoclgft  3564  moi2  3738  preq12bg  4878  disjxiun  5163  disjxun  5164  wereu2  5697  frpomin  6372  f1ocnv2d  7703  funeldmdif  8089  extmptsuppeq  8229  suppssr  8236  suppssrg  8237  omeulem1  8638  oelim2  8651  oeoa  8653  boxriin  8998  frfi  9349  fipreima  9428  marypha1lem  9502  supiso  9544  ordtypelem10  9596  r1ordg  9847  infxpenc2lem1  10088  acndom  10120  acndom2  10123  cofsmo  10338  cfcoflem  10341  fin23lem28  10409  fin23lem36  10417  isf32lem1  10422  isf32lem2  10423  isf32lem5  10426  isf34lem4  10446  fin1a2lem6  10474  fin1a2s  10483  ttukeylem2  10579  ttukeylem6  10583  fpwwe2lem7  10706  fpwwe2lem11  10710  inar1  10844  grudomon  10886  axpre-sup  11238  un0addcl  12586  un0mulcl  12587  peano2uz2  12731  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  xlemul1a  13350  fzadd2  13619  elfz2nn0  13675  fzind2  13835  expaddz  14157  expmulz  14159  swrdswrd  14753  cau3lem  15403  lo1bdd2  15570  climuni  15598  fsumcom2  15822  fprodcom2  16032  dvdsval2  16305  algcvga  16626  lcmgcdlem  16653  coprmproddvdslem  16709  divgcdcoprmex  16713  iserodd  16882  prmpwdvds  16951  ram0  17069  catpropd  17767  mndind  18863  isgrpinv  19033  gicsubgen  19319  sylow2alem2  19660  sylow2a  19661  frgpuptinv  19813  gsumcom3fi  20021  gsumxp2  20022  ablfac1eu  20117  dvdsrcl2  20392  islss4  20983  ellspsn6  21015  lmhmima  21069  lsmcl  21105  psgnodpm  21629  dsmmlss  21787  islindf4  21881  gsumbagdiag  21974  psrass1lem  21975  coe1tmmul2  22300  dmatscmcl  22530  mdetdiaglem  22625  mdetunilem9  22647  pm2mp  22852  epttop  23037  neindisj  23146  neitr  23209  restcls  23210  restntr  23211  ordtrest2lem  23232  cncnp  23309  cnconst  23313  1stcrest  23482  2ndcdisj  23485  2ndcsep  23488  1stccnp  23491  islly2  23513  1stckgenlem  23582  ptbasin  23606  ptbasfi  23610  ptcnplem  23650  ptcnp  23651  tx1stc  23679  qtophmeo  23846  filconn  23912  filuni  23914  ufileu  23948  elfm3  23979  rnelfmlem  23981  fmfnfmlem4  23986  cnpflf2  24029  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem4  24084  ptcmplem5  24085  tsmsxplem1  24182  bl2in  24431  metcnpi  24578  metcnpi2  24579  metcnpi3  24580  recld2  24855  icoopnst  24988  iocopnst  24989  ncvs1  25210  iscfil3  25326  iscmet3lem2  25345  ovoliunlem1  25556  ovolicc2lem2  25572  ovolicc2lem4  25574  voliun  25608  volsuplem  25609  dyadmbllem  25653  mbfinf  25719  mbflimsup  25720  itg2seq  25797  itg2splitlem  25803  itg2cnlem1  25816  ellimc3  25934  dvnadd  25985  dvcnvlem  26034  c1liplem1  26055  lhop2  26074  coe1mul3  26158  ply1divex  26196  dvdsq1p  26222  aannenlem1  26388  aalioulem2  26393  dvtaylp  26430  ulmdvlem3  26463  iblulm  26468  cxpmul2z  26751  xrlimcnp  27029  lgambdd  27098  wilthlem2  27130  basellem3  27144  dvdsflsumcom  27249  perfect  27293  dchreq  27320  dchrsum  27331  bposlem1  27346  lgsquad2  27448  dchrisum0fno1  27573  pntibnd  27655  noinfbnd1lem4  27789  cuteq1  27896  madebdaylemlrcut  27955  precsexlem11  28259  recsex  28261  noseqp1  28315  noseqrdgfn  28330  remulscllem2  28451  oppperpex  28779  lmieu  28810  ax5seglem5  28966  axeuclid  28996  egrsubgr  29312  nbumgrvtx  29381  wwlksnextsurj  29933  clwwlkccat  30022  numclwwlk2lem1lem  30374  nmcvcn  30727  ubthlem1  30902  leopmul2i  32167  hstel2  32251  atom1d  32385  cdj1i  32465  f1o3d  32646  fsuppcurry1  32739  fsuppcurry2  32740  xrge0addge  32764  isdrng4  33264  prmidl0  33443  mxidlmax  33458  reff  33785  ordtrest2NEWlem  33868  esumcst  34027  eulerpartlemgh  34343  cvmscld  35241  cgrxfr  36019  finminlem  36284  nn0prpwlem  36288  neibastop1  36325  neibastop2lem  36326  tailfb  36343  fvineqsneu  37377  pibt2  37383  finixpnum  37565  lindsenlbs  37575  matunitlindflem2  37577  poimirlem4  37584  poimirlem25  37605  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  heicant  37615  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2addnclem3  37633  ftc1anc  37661  subspopn  37712  prdsbnd  37753  heibor1lem  37769  heiborlem1  37771  heibor  37781  isdrngo2  37918  rngoisocnv  37941  maxidlmax  38003  riotasv3d  38916  lkrpssN  39119  intnatN  39364  elpaddatiN  39762  pexmidlem5N  39931  lhpj1  39979  ltrnu  40078  cdlemn11pre  41167  dihord2pre  41182  dih1dimatlem0  41285  lcfrlem9  41507  remulcand  42414  prjspner1  42581  0prjspnrel  42582  nna4b4nsq  42615  rexrabdioph  42750  ctbnfien  42774  irrapxlem3  42780  elpell14qr2  42818  elpell1qr2  42828  kelac1  43020  iunrelexpuztr  43681  rfovcnvfvd  43969  radcnvrat  44283  nznngen  44285  tz6.12-afv  47088  tz6.12-afv2  47155  iccelpart  47307  prproropf1olem3  47379  lighneallem4  47484  perfectALTV  47597  bgoldbtbndlem3  47681  tgoldbach  47691  isuspgrim0  47756  uspgrimprop  47757  grimcnv  47763  grimco  47764  grimedg  47787  isassintop  47933  ellcoellss  48164  lindslinindsimp2  48192  itscnhlinecirc02plem3  48518  inlinecirc02p  48521  aacllem  48895