Theorem impr 457

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 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 421	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reximddv2  3280  moi2  3709  preq12bg  4786  disjxiun  5065  disjxun  5066  wereu2  5554  f1ocnv2d  7400  funeldmdif  7749  extmptsuppeq  7856  suppssr  7863  omeulem1  8210  oelim2  8223  oeoa  8225  boxriin  8506  frfi  8765  fipreima  8832  marypha1lem  8899  supiso  8941  ordtypelem10  8993  r1ordg  9209  infxpenc2lem1  9447  acndom  9479  acndom2  9482  cofsmo  9693  cfcoflem  9696  fin23lem28  9764  fin23lem36  9772  isf32lem1  9777  isf32lem2  9778  isf32lem5  9781  isf34lem4  9801  fin1a2lem6  9829  fin1a2s  9838  ttukeylem2  9934  ttukeylem6  9938  fpwwe2lem8  10061  fpwwe2lem12  10065  inar1  10199  grudomon  10241  axpre-sup  10593  un0addcl  11933  un0mulcl  11934  peano2uz2  12073  rpnnen1lem2  12379  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  xlemul1a  12684  fzadd2  12945  elfz2nn0  13001  fzind2  13158  expaddz  13476  expmulz  13478  swrdswrd  14069  cau3lem  14716  lo1bdd2  14883  climuni  14911  fsumcom2  15131  fprodcom2  15340  dvdsval2  15612  algcvga  15925  lcmgcdlem  15952  coprmproddvdslem  16008  divgcdcoprmex  16012  iserodd  16174  prmpwdvds  16242  ram0  16360  catpropd  16981  mndind  17994  isgrpinv  18158  gicsubgen  18420  sylow2alem2  18745  sylow2a  18746  frgpuptinv  18899  gsumcom3fi  19101  gsumxp2  19102  ablfac1eu  19197  dvdsrcl2  19402  islss4  19736  lspsnel6  19768  lmhmima  19821  lsmcl  19857  gsumbagdiag  20158  psrass1lem  20159  coe1tmmul2  20446  psgnodpm  20734  dsmmlss  20890  islindf4  20984  dmatscmcl  21114  mdetdiaglem  21209  mdetunilem9  21231  pm2mp  21435  epttop  21619  neindisj  21727  neitr  21790  restcls  21791  restntr  21792  ordtrest2lem  21813  cncnp  21890  cnconst  21894  1stcrest  22063  2ndcdisj  22066  2ndcsep  22069  1stccnp  22072  islly2  22094  1stckgenlem  22163  ptbasin  22187  ptbasfi  22191  ptcnplem  22231  ptcnp  22232  tx1stc  22260  qtophmeo  22427  filconn  22493  filuni  22495  ufileu  22529  elfm3  22560  rnelfmlem  22562  fmfnfmlem4  22567  cnpflf2  22610  alexsubALTlem4  22660  ptcmplem3  22664  ptcmplem4  22665  ptcmplem5  22666  tsmsxplem1  22763  bl2in  23012  metcnpi  23156  metcnpi2  23157  metcnpi3  23158  recld2  23424  icoopnst  23545  iocopnst  23546  ncvs1  23763  iscfil3  23878  iscmet3lem2  23897  ovoliunlem1  24105  ovolicc2lem2  24121  ovolicc2lem4  24123  voliun  24157  volsuplem  24158  dyadmbllem  24202  mbfinf  24268  mbflimsup  24269  itg2seq  24345  itg2splitlem  24351  itg2cnlem1  24364  ellimc3  24479  dvnadd  24528  dvcnvlem  24575  c1liplem1  24595  lhop2  24614  coe1mul3  24695  ply1divex  24732  dvdsq1p  24756  aannenlem1  24919  aalioulem2  24924  dvtaylp  24960  ulmdvlem3  24992  iblulm  24997  cxpmul2z  25276  xrlimcnp  25548  lgambdd  25616  wilthlem2  25648  basellem3  25662  dvdsflsumcom  25767  perfect  25809  dchreq  25836  dchrsum  25847  bposlem1  25862  lgsquad2  25964  dchrisum0fno1  26089  pntibnd  26171  oppperpex  26541  lmieu  26572  ax5seglem5  26721  axeuclid  26751  egrsubgr  27061  nbumgrvtx  27130  wwlksnextsurj  27680  clwwlkccat  27770  numclwwlk2lem1lem  28123  nmcvcn  28474  ubthlem1  28649  leopmul2i  29914  hstel2  29998  atom1d  30132  cdj1i  30212  f1o3d  30374  fsuppcurry1  30463  fsuppcurry2  30464  xrge0addge  30483  mxidlmax  30976  reff  31105  ordtrest2NEWlem  31167  esumcst  31324  eulerpartlemgh  31638  cvmscld  32522  frpomin  33080  cgrxfr  33518  finminlem  33668  nn0prpwlem  33672  neibastop1  33709  neibastop2lem  33710  tailfb  33727  fvineqsneu  34694  pibt2  34700  finixpnum  34879  lindsenlbs  34889  matunitlindflem2  34891  poimirlem4  34898  poimirlem25  34919  poimirlem26  34920  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  heicant  34929  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem  34945  itg2addnclem3  34947  ftc1anc  34977  subspopn  35029  prdsbnd  35073  heibor1lem  35089  heiborlem1  35091  heibor  35101  isdrngo2  35238  rngoisocnv  35261  maxidlmax  35323  riotasv3d  36098  lkrpssN  36301  intnatN  36545  elpaddatiN  36943  pexmidlem5N  37112  lhpj1  37160  ltrnu  37259  cdlemn11pre  38348  dihord2pre  38363  dih1dimatlem0  38466  lcfrlem9  38688  remulcand  39257  0prjspnrel  39276  rexrabdioph  39398  ctbnfien  39422  irrapxlem3  39428  elpell14qr2  39466  elpell1qr2  39476  kelac1  39670  iunrelexpuztr  40071  rfovcnvfvd  40360  radcnvrat  40653  nznngen  40655  tz6.12-afv  43379  tz6.12-afv2  43446  iccelpart  43600  prproropf1olem3  43674  lighneallem4  43782  perfectALTV  43895  bgoldbtbndlem3  43979  tgoldbach  43989  isomuspgr  44006  isassintop  44124  ellcoellss  44497  lindslinindsimp2  44525  itscnhlinecirc02plem3  44778  inlinecirc02p  44781  aacllem  44909