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  3188  vtoclgft  3507  moi2  3676  preq12bg  4804  disjxiun  5089  disjxun  5090  wereu2  5616  frpomin  6288  f1ocnv2d  7602  funeldmdif  7983  extmptsuppeq  8121  suppssr  8128  suppssrg  8129  omeulem1  8500  oelim2  8513  oeoa  8515  boxriin  8867  frfi  9174  fipreima  9248  marypha1lem  9323  supiso  9366  ordtypelem10  9419  r1ordg  9674  infxpenc2lem1  9913  acndom  9945  acndom2  9948  cofsmo  10163  cfcoflem  10166  fin23lem28  10234  fin23lem36  10242  isf32lem1  10247  isf32lem2  10248  isf32lem5  10251  isf34lem4  10271  fin1a2lem6  10299  fin1a2s  10308  ttukeylem2  10404  ttukeylem6  10408  fpwwe2lem7  10531  fpwwe2lem11  10535  inar1  10669  grudomon  10711  axpre-sup  11063  un0addcl  12417  un0mulcl  12418  peano2uz2  12564  rpnnen1lem2  12878  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  xlemul1a  13190  fzadd2  13462  elfz2nn0  13521  fzind2  13688  expaddz  14013  expmulz  14015  swrdswrd  14611  cau3lem  15262  lo1bdd2  15431  climuni  15459  fsumcom2  15681  fprodcom2  15891  dvdsval2  16166  algcvga  16490  lcmgcdlem  16517  coprmproddvdslem  16573  divgcdcoprmex  16577  iserodd  16747  prmpwdvds  16816  ram0  16934  catpropd  17615  mndind  18702  isgrpinv  18872  gicsubgen  19158  sylow2alem2  19497  sylow2a  19498  frgpuptinv  19650  gsumcom3fi  19858  gsumxp2  19859  ablfac1eu  19954  dvdsrcl2  20251  islss4  20865  ellspsn6  20897  lmhmima  20951  lsmcl  20987  psgnodpm  21495  dsmmlss  21651  islindf4  21745  gsumbagdiag  21838  psrass1lem  21839  coe1tmmul2  22160  dmatscmcl  22388  mdetdiaglem  22483  mdetunilem9  22505  pm2mp  22710  epttop  22894  neindisj  23002  neitr  23065  restcls  23066  restntr  23067  ordtrest2lem  23088  cncnp  23165  cnconst  23169  1stcrest  23338  2ndcdisj  23341  2ndcsep  23344  1stccnp  23347  islly2  23369  1stckgenlem  23438  ptbasin  23462  ptbasfi  23466  ptcnplem  23506  ptcnp  23507  tx1stc  23535  qtophmeo  23702  filconn  23768  filuni  23770  ufileu  23804  elfm3  23835  rnelfmlem  23837  fmfnfmlem4  23842  cnpflf2  23885  alexsubALTlem4  23935  ptcmplem3  23939  ptcmplem4  23940  ptcmplem5  23941  tsmsxplem1  24038  bl2in  24286  metcnpi  24430  metcnpi2  24431  metcnpi3  24432  recld2  24701  icoopnst  24834  iocopnst  24835  ncvs1  25055  iscfil3  25171  iscmet3lem2  25190  ovoliunlem1  25401  ovolicc2lem2  25417  ovolicc2lem4  25419  voliun  25453  volsuplem  25454  dyadmbllem  25498  mbfinf  25564  mbflimsup  25565  itg2seq  25641  itg2splitlem  25647  itg2cnlem1  25660  ellimc3  25778  dvnadd  25829  dvcnvlem  25878  c1liplem1  25899  lhop2  25918  coe1mul3  26002  ply1divex  26040  dvdsq1p  26066  aannenlem1  26234  aalioulem2  26239  dvtaylp  26276  ulmdvlem3  26309  iblulm  26314  cxpmul2z  26598  xrlimcnp  26876  lgambdd  26945  wilthlem2  26977  basellem3  26991  dvdsflsumcom  27096  perfect  27140  dchreq  27167  dchrsum  27178  bposlem1  27193  lgsquad2  27295  dchrisum0fno1  27420  pntibnd  27502  noinfbnd1lem4  27636  cuteq1  27748  madebdaylemlrcut  27813  precsexlem11  28124  recsex  28126  bdayon  28178  noseqp1  28190  noseqrdgfn  28205  remulscllem2  28370  oppperpex  28698  lmieu  28729  ax5seglem5  28878  axeuclid  28908  egrsubgr  29222  nbumgrvtx  29291  wwlksnextsurj  29845  clwwlkccat  29934  numclwwlk2lem1lem  30286  nmcvcn  30639  ubthlem1  30814  leopmul2i  32079  hstel2  32163  atom1d  32297  cdj1i  32377  f1o3d  32570  fsuppcurry1  32669  fsuppcurry2  32670  xrge0addge  32702  isdrng4  33235  prmidl0  33388  mxidlmax  33403  reff  33812  ordtrest2NEWlem  33895  esumcst  34036  eulerpartlemgh  34352  cvmscld  35256  cgrxfr  36039  finminlem  36302  nn0prpwlem  36306  neibastop1  36343  neibastop2lem  36344  tailfb  36361  fvineqsneu  37395  pibt2  37401  finixpnum  37595  lindsenlbs  37605  matunitlindflem2  37607  poimirlem4  37614  poimirlem25  37635  poimirlem26  37636  poimirlem29  37639  poimirlem30  37640  poimirlem31  37641  poimirlem32  37642  heicant  37645  mblfinlem3  37649  mblfinlem4  37650  itg2addnclem  37661  itg2addnclem3  37663  ftc1anc  37691  subspopn  37742  prdsbnd  37783  heibor1lem  37799  heiborlem1  37801  heibor  37811  isdrngo2  37948  rngoisocnv  37971  maxidlmax  38033  riotasv3d  38949  lkrpssN  39152  intnatN  39396  elpaddatiN  39794  pexmidlem5N  39963  lhpj1  40011  ltrnu  40110  cdlemn11pre  41199  dihord2pre  41214  dih1dimatlem0  41317  lcfrlem9  41539  remulcand  42422  prjspner1  42609  0prjspnrel  42610  nna4b4nsq  42643  rexrabdioph  42777  ctbnfien  42801  irrapxlem3  42807  elpell14qr2  42845  elpell1qr2  42855  kelac1  43046  iunrelexpuztr  43702  rfovcnvfvd  43990  radcnvrat  44297  nznngen  44299  tz6.12-afv  47167  tz6.12-afv2  47234  iccelpart  47427  prproropf1olem3  47499  lighneallem4  47604  perfectALTV  47717  bgoldbtbndlem3  47801  tgoldbach  47811  grimcnv  47882  grimco  47883  isuspgrim0  47888  grimedg  47929  isubgr3stgrlem7  47966  gpg5nbgrvtx03starlem1  48062  gpg5nbgrvtx03starlem3  48064  gpg5nbgrvtx13starlem1  48065  gpg5nbgrvtx13starlem3  48067  isassintop  48204  ellcoellss  48430  lindslinindsimp2  48458  itscnhlinecirc02plem3  48779  inlinecirc02p  48782  aacllem  49796