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  3196  vtoclgft  3518  moi2  3687  preq12bg  4817  disjxiun  5104  disjxun  5105  wereu2  5635  frpomin  6313  f1ocnv2d  7642  funeldmdif  8027  extmptsuppeq  8167  suppssr  8174  suppssrg  8175  omeulem1  8546  oelim2  8559  oeoa  8561  boxriin  8913  frfi  9232  fipreima  9309  marypha1lem  9384  supiso  9427  ordtypelem10  9480  r1ordg  9731  infxpenc2lem1  9972  acndom  10004  acndom2  10007  cofsmo  10222  cfcoflem  10225  fin23lem28  10293  fin23lem36  10301  isf32lem1  10306  isf32lem2  10307  isf32lem5  10310  isf34lem4  10330  fin1a2lem6  10358  fin1a2s  10367  ttukeylem2  10463  ttukeylem6  10467  fpwwe2lem7  10590  fpwwe2lem11  10594  inar1  10728  grudomon  10770  axpre-sup  11122  un0addcl  12475  un0mulcl  12476  peano2uz2  12622  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  xlemul1a  13248  fzadd2  13520  elfz2nn0  13579  fzind2  13746  expaddz  14071  expmulz  14073  swrdswrd  14670  cau3lem  15321  lo1bdd2  15490  climuni  15518  fsumcom2  15740  fprodcom2  15950  dvdsval2  16225  algcvga  16549  lcmgcdlem  16576  coprmproddvdslem  16632  divgcdcoprmex  16636  iserodd  16806  prmpwdvds  16875  ram0  16993  catpropd  17670  mndind  18755  isgrpinv  18925  gicsubgen  19211  sylow2alem2  19548  sylow2a  19549  frgpuptinv  19701  gsumcom3fi  19909  gsumxp2  19910  ablfac1eu  20005  dvdsrcl2  20275  islss4  20868  ellspsn6  20900  lmhmima  20954  lsmcl  20990  psgnodpm  21497  dsmmlss  21653  islindf4  21747  gsumbagdiag  21840  psrass1lem  21841  coe1tmmul2  22162  dmatscmcl  22390  mdetdiaglem  22485  mdetunilem9  22507  pm2mp  22712  epttop  22896  neindisj  23004  neitr  23067  restcls  23068  restntr  23069  ordtrest2lem  23090  cncnp  23167  cnconst  23171  1stcrest  23340  2ndcdisj  23343  2ndcsep  23346  1stccnp  23349  islly2  23371  1stckgenlem  23440  ptbasin  23464  ptbasfi  23468  ptcnplem  23508  ptcnp  23509  tx1stc  23537  qtophmeo  23704  filconn  23770  filuni  23772  ufileu  23806  elfm3  23837  rnelfmlem  23839  fmfnfmlem4  23844  cnpflf2  23887  alexsubALTlem4  23937  ptcmplem3  23941  ptcmplem4  23942  ptcmplem5  23943  tsmsxplem1  24040  bl2in  24288  metcnpi  24432  metcnpi2  24433  metcnpi3  24434  recld2  24703  icoopnst  24836  iocopnst  24837  ncvs1  25057  iscfil3  25173  iscmet3lem2  25192  ovoliunlem1  25403  ovolicc2lem2  25419  ovolicc2lem4  25421  voliun  25455  volsuplem  25456  dyadmbllem  25500  mbfinf  25566  mbflimsup  25567  itg2seq  25643  itg2splitlem  25649  itg2cnlem1  25662  ellimc3  25780  dvnadd  25831  dvcnvlem  25880  c1liplem1  25901  lhop2  25920  coe1mul3  26004  ply1divex  26042  dvdsq1p  26068  aannenlem1  26236  aalioulem2  26241  dvtaylp  26278  ulmdvlem3  26311  iblulm  26316  cxpmul2z  26600  xrlimcnp  26878  lgambdd  26947  wilthlem2  26979  basellem3  26993  dvdsflsumcom  27098  perfect  27142  dchreq  27169  dchrsum  27180  bposlem1  27195  lgsquad2  27297  dchrisum0fno1  27422  pntibnd  27504  noinfbnd1lem4  27638  cuteq1  27746  madebdaylemlrcut  27810  precsexlem11  28119  recsex  28121  bdayon  28173  noseqp1  28185  noseqrdgfn  28200  remulscllem2  28352  oppperpex  28680  lmieu  28711  ax5seglem5  28860  axeuclid  28890  egrsubgr  29204  nbumgrvtx  29273  wwlksnextsurj  29830  clwwlkccat  29919  numclwwlk2lem1lem  30271  nmcvcn  30624  ubthlem1  30799  leopmul2i  32064  hstel2  32148  atom1d  32282  cdj1i  32362  f1o3d  32551  fsuppcurry1  32648  fsuppcurry2  32649  xrge0addge  32681  isdrng4  33245  prmidl0  33421  mxidlmax  33436  reff  33829  ordtrest2NEWlem  33912  esumcst  34053  eulerpartlemgh  34369  cvmscld  35260  cgrxfr  36043  finminlem  36306  nn0prpwlem  36310  neibastop1  36347  neibastop2lem  36348  tailfb  36365  fvineqsneu  37399  pibt2  37405  finixpnum  37599  lindsenlbs  37609  matunitlindflem2  37611  poimirlem4  37618  poimirlem25  37639  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2addnclem3  37667  ftc1anc  37695  subspopn  37746  prdsbnd  37787  heibor1lem  37803  heiborlem1  37805  heibor  37815  isdrngo2  37952  rngoisocnv  37975  maxidlmax  38037  riotasv3d  38953  lkrpssN  39156  intnatN  39401  elpaddatiN  39799  pexmidlem5N  39968  lhpj1  40016  ltrnu  40115  cdlemn11pre  41204  dihord2pre  41219  dih1dimatlem0  41322  lcfrlem9  41544  remulcand  42427  prjspner1  42614  0prjspnrel  42615  nna4b4nsq  42648  rexrabdioph  42782  ctbnfien  42806  irrapxlem3  42812  elpell14qr2  42850  elpell1qr2  42860  kelac1  43052  iunrelexpuztr  43708  rfovcnvfvd  43996  radcnvrat  44303  nznngen  44305  tz6.12-afv  47174  tz6.12-afv2  47241  iccelpart  47434  prproropf1olem3  47506  lighneallem4  47611  perfectALTV  47724  bgoldbtbndlem3  47808  tgoldbach  47818  grimcnv  47888  grimco  47889  isuspgrim0  47894  grimedg  47935  isubgr3stgrlem7  47971  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  isassintop  48198  ellcoellss  48424  lindslinindsimp2  48452  itscnhlinecirc02plem3  48773  inlinecirc02p  48776  aacllem  49790