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  3278  moi2  3707  preq12bg  4784  disjxiun  5063  disjxun  5064  wereu2  5552  f1ocnv2d  7398  funeldmdif  7747  extmptsuppeq  7854  suppssr  7861  omeulem1  8208  oelim2  8221  oeoa  8223  boxriin  8504  frfi  8763  fipreima  8830  marypha1lem  8897  supiso  8939  ordtypelem10  8991  r1ordg  9207  infxpenc2lem1  9445  acndom  9477  acndom2  9480  cofsmo  9691  cfcoflem  9694  fin23lem28  9762  fin23lem36  9770  isf32lem1  9775  isf32lem2  9776  isf32lem5  9779  isf34lem4  9799  fin1a2lem6  9827  fin1a2s  9836  ttukeylem2  9932  ttukeylem6  9936  fpwwe2lem8  10059  fpwwe2lem12  10063  inar1  10197  grudomon  10239  axpre-sup  10591  un0addcl  11931  un0mulcl  11932  peano2uz2  12071  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  xlemul1a  12682  fzadd2  12943  elfz2nn0  12999  fzind2  13156  expaddz  13474  expmulz  13476  swrdswrd  14067  cau3lem  14714  lo1bdd2  14881  climuni  14909  fsumcom2  15129  fprodcom2  15338  dvdsval2  15610  algcvga  15923  lcmgcdlem  15950  coprmproddvdslem  16006  divgcdcoprmex  16010  iserodd  16172  prmpwdvds  16240  ram0  16358  catpropd  16979  mndind  17992  isgrpinv  18156  gicsubgen  18418  sylow2alem2  18743  sylow2a  18744  frgpuptinv  18897  gsumcom3fi  19099  gsumxp2  19100  ablfac1eu  19195  dvdsrcl2  19400  islss4  19734  lspsnel6  19766  lmhmima  19819  lsmcl  19855  gsumbagdiag  20156  psrass1lem  20157  coe1tmmul2  20444  psgnodpm  20732  dsmmlss  20888  islindf4  20982  dmatscmcl  21112  mdetdiaglem  21207  mdetunilem9  21229  pm2mp  21433  epttop  21617  neindisj  21725  neitr  21788  restcls  21789  restntr  21790  ordtrest2lem  21811  cncnp  21888  cnconst  21892  1stcrest  22061  2ndcdisj  22064  2ndcsep  22067  1stccnp  22070  islly2  22092  1stckgenlem  22161  ptbasin  22185  ptbasfi  22189  ptcnplem  22229  ptcnp  22230  tx1stc  22258  qtophmeo  22425  filconn  22491  filuni  22493  ufileu  22527  elfm3  22558  rnelfmlem  22560  fmfnfmlem4  22565  cnpflf2  22608  alexsubALTlem4  22658  ptcmplem3  22662  ptcmplem4  22663  ptcmplem5  22664  tsmsxplem1  22761  bl2in  23010  metcnpi  23154  metcnpi2  23155  metcnpi3  23156  recld2  23422  icoopnst  23543  iocopnst  23544  ncvs1  23761  iscfil3  23876  iscmet3lem2  23895  ovoliunlem1  24103  ovolicc2lem2  24119  ovolicc2lem4  24121  voliun  24155  volsuplem  24156  dyadmbllem  24200  mbfinf  24266  mbflimsup  24267  itg2seq  24343  itg2splitlem  24349  itg2cnlem1  24362  ellimc3  24477  dvnadd  24526  dvcnvlem  24573  c1liplem1  24593  lhop2  24612  coe1mul3  24693  ply1divex  24730  dvdsq1p  24754  aannenlem1  24917  aalioulem2  24922  dvtaylp  24958  ulmdvlem3  24990  iblulm  24995  cxpmul2z  25274  xrlimcnp  25546  lgambdd  25614  wilthlem2  25646  basellem3  25660  dvdsflsumcom  25765  perfect  25807  dchreq  25834  dchrsum  25845  bposlem1  25860  lgsquad2  25962  dchrisum0fno1  26087  pntibnd  26169  oppperpex  26539  lmieu  26570  ax5seglem5  26719  axeuclid  26749  egrsubgr  27059  nbumgrvtx  27128  wwlksnextsurj  27678  clwwlkccat  27768  numclwwlk2lem1lem  28121  nmcvcn  28472  ubthlem1  28647  leopmul2i  29912  hstel2  29996  atom1d  30130  cdj1i  30210  f1o3d  30372  fsuppcurry1  30461  fsuppcurry2  30462  xrge0addge  30481  mxidlmax  30974  reff  31103  ordtrest2NEWlem  31165  esumcst  31322  eulerpartlemgh  31636  cvmscld  32520  frpomin  33078  cgrxfr  33516  finminlem  33666  nn0prpwlem  33670  neibastop1  33707  neibastop2lem  33708  tailfb  33725  fvineqsneu  34695  pibt2  34701  finixpnum  34892  lindsenlbs  34902  matunitlindflem2  34904  poimirlem4  34911  poimirlem25  34932  poimirlem26  34933  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  heicant  34942  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  itg2addnclem3  34960  ftc1anc  34990  subspopn  35042  prdsbnd  35086  heibor1lem  35102  heiborlem1  35104  heibor  35114  isdrngo2  35251  rngoisocnv  35274  maxidlmax  35336  riotasv3d  36111  lkrpssN  36314  intnatN  36558  elpaddatiN  36956  pexmidlem5N  37125  lhpj1  37173  ltrnu  37272  cdlemn11pre  38361  dihord2pre  38376  dih1dimatlem0  38479  lcfrlem9  38701  remulcand  39270  0prjspnrel  39289  rexrabdioph  39411  ctbnfien  39435  irrapxlem3  39441  elpell14qr2  39479  elpell1qr2  39489  kelac1  39683  iunrelexpuztr  40084  rfovcnvfvd  40373  radcnvrat  40666  nznngen  40668  tz6.12-afv  43392  tz6.12-afv2  43459  iccelpart  43613  prproropf1olem3  43687  lighneallem4  43795  perfectALTV  43908  bgoldbtbndlem3  43992  tgoldbach  44002  isomuspgr  44019  isassintop  44137  ellcoellss  44510  lindslinindsimp2  44538  itscnhlinecirc02plem3  44791  inlinecirc02p  44794  aacllem  44922