Theorem impr 456

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  reximddv2  3213  moi2  3713  preq12bg  4855  disjxiun  5146  disjxun  5147  wereu2  5674  frpomin  6342  f1ocnv2d  7659  funeldmdif  8034  extmptsuppeq  8173  suppssr  8181  suppssrg  8182  omeulem1  8582  oelim2  8595  oeoa  8597  boxriin  8934  frfi  9288  fipreima  9358  marypha1lem  9428  supiso  9470  ordtypelem10  9522  r1ordg  9773  infxpenc2lem1  10014  acndom  10046  acndom2  10049  cofsmo  10264  cfcoflem  10267  fin23lem28  10335  fin23lem36  10343  isf32lem1  10348  isf32lem2  10349  isf32lem5  10352  isf34lem4  10372  fin1a2lem6  10400  fin1a2s  10409  ttukeylem2  10505  ttukeylem6  10509  fpwwe2lem7  10632  fpwwe2lem11  10636  inar1  10770  grudomon  10812  axpre-sup  11164  un0addcl  12505  un0mulcl  12506  peano2uz2  12650  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  xlemul1a  13267  fzadd2  13536  elfz2nn0  13592  fzind2  13750  expaddz  14072  expmulz  14074  swrdswrd  14655  cau3lem  15301  lo1bdd2  15468  climuni  15496  fsumcom2  15720  fprodcom2  15928  dvdsval2  16200  algcvga  16516  lcmgcdlem  16543  coprmproddvdslem  16599  divgcdcoprmex  16603  iserodd  16768  prmpwdvds  16837  ram0  16955  catpropd  17653  mndind  18709  isgrpinv  18878  gicsubgen  19152  sylow2alem2  19486  sylow2a  19487  frgpuptinv  19639  gsumcom3fi  19847  gsumxp2  19848  ablfac1eu  19943  dvdsrcl2  20180  islss4  20573  lspsnel6  20605  lmhmima  20658  lsmcl  20694  psgnodpm  21141  dsmmlss  21299  islindf4  21393  gsumbagdiagOLD  21492  psrass1lemOLD  21493  gsumbagdiag  21495  psrass1lem  21496  coe1tmmul2  21798  dmatscmcl  22005  mdetdiaglem  22100  mdetunilem9  22122  pm2mp  22327  epttop  22512  neindisj  22621  neitr  22684  restcls  22685  restntr  22686  ordtrest2lem  22707  cncnp  22784  cnconst  22788  1stcrest  22957  2ndcdisj  22960  2ndcsep  22963  1stccnp  22966  islly2  22988  1stckgenlem  23057  ptbasin  23081  ptbasfi  23085  ptcnplem  23125  ptcnp  23126  tx1stc  23154  qtophmeo  23321  filconn  23387  filuni  23389  ufileu  23423  elfm3  23454  rnelfmlem  23456  fmfnfmlem4  23461  cnpflf2  23504  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem4  23559  ptcmplem5  23560  tsmsxplem1  23657  bl2in  23906  metcnpi  24053  metcnpi2  24054  metcnpi3  24055  recld2  24330  icoopnst  24455  iocopnst  24456  ncvs1  24674  iscfil3  24790  iscmet3lem2  24809  ovoliunlem1  25019  ovolicc2lem2  25035  ovolicc2lem4  25037  voliun  25071  volsuplem  25072  dyadmbllem  25116  mbfinf  25182  mbflimsup  25183  itg2seq  25260  itg2splitlem  25266  itg2cnlem1  25279  ellimc3  25396  dvnadd  25446  dvcnvlem  25493  c1liplem1  25513  lhop2  25532  coe1mul3  25617  ply1divex  25654  dvdsq1p  25678  aannenlem1  25841  aalioulem2  25846  dvtaylp  25882  ulmdvlem3  25914  iblulm  25919  cxpmul2z  26199  xrlimcnp  26473  lgambdd  26541  wilthlem2  26573  basellem3  26587  dvdsflsumcom  26692  perfect  26734  dchreq  26761  dchrsum  26772  bposlem1  26787  lgsquad2  26889  dchrisum0fno1  27014  pntibnd  27096  noinfbnd1lem4  27229  cuteq1  27334  madebdaylemlrcut  27393  precsexlem11  27663  recsex  27665  oppperpex  28004  lmieu  28035  ax5seglem5  28191  axeuclid  28221  egrsubgr  28534  nbumgrvtx  28603  wwlksnextsurj  29154  clwwlkccat  29243  numclwwlk2lem1lem  29595  nmcvcn  29948  ubthlem1  30123  leopmul2i  31388  hstel2  31472  atom1d  31606  cdj1i  31686  f1o3d  31851  fsuppcurry1  31950  fsuppcurry2  31951  xrge0addge  31970  isdrng4  32395  prmidl0  32569  mxidlmax  32581  reff  32819  ordtrest2NEWlem  32902  esumcst  33061  eulerpartlemgh  33377  cvmscld  34264  cgrxfr  35027  finminlem  35203  nn0prpwlem  35207  neibastop1  35244  neibastop2lem  35245  tailfb  35262  fvineqsneu  36292  pibt2  36298  finixpnum  36473  lindsenlbs  36483  matunitlindflem2  36485  poimirlem4  36492  poimirlem25  36513  poimirlem26  36514  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  heicant  36523  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  itg2addnclem3  36541  ftc1anc  36569  subspopn  36620  prdsbnd  36661  heibor1lem  36677  heiborlem1  36679  heibor  36689  isdrngo2  36826  rngoisocnv  36849  maxidlmax  36911  riotasv3d  37830  lkrpssN  38033  intnatN  38278  elpaddatiN  38676  pexmidlem5N  38845  lhpj1  38893  ltrnu  38992  cdlemn11pre  40081  dihord2pre  40096  dih1dimatlem0  40199  lcfrlem9  40421  remulcand  41311  prjspner1  41368  0prjspnrel  41369  nna4b4nsq  41402  rexrabdioph  41532  ctbnfien  41556  irrapxlem3  41562  elpell14qr2  41600  elpell1qr2  41610  kelac1  41805  iunrelexpuztr  42470  rfovcnvfvd  42758  radcnvrat  43073  nznngen  43075  tz6.12-afv  45881  tz6.12-afv2  45948  iccelpart  46101  prproropf1olem3  46173  lighneallem4  46278  perfectALTV  46391  bgoldbtbndlem3  46475  tgoldbach  46485  isomuspgr  46502  isassintop  46620  ellcoellss  47116  lindslinindsimp2  47144  itscnhlinecirc02plem3  47470  inlinecirc02p  47473  aacllem  47848