Theorem impr 460

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reximddv2  3221  vtoclgft  3515  moi2  3673  preq12bg  4812  disjxiun  5099  disjxun  5100  wereu2  5647  frpomin  6343  f1ocnv2d  7674  funeldmdif  8059  extmptsuppeq  8205  suppssr  8212  suppssrg  8213  omeulem1  8590  oelim2  8604  oeoa  8606  boxriin  8968  frfi  9276  fipreima  9347  marypha1lem  9425  supiso  9468  ordtypelem10  9521  r1ordg  9785  infxpenc2lem1  10098  acndom  10130  acndom2  10133  cofsmo  10347  cfcoflem  10350  fin23lem28  10418  fin23lem36  10426  isf32lem1  10431  isf32lem2  10432  isf32lem5  10435  isf34lem4  10455  fin1a2lem6  10483  fin1a2s  10492  ttukeylem2  10588  ttukeylem6  10592  fpwwe2lem7  10722  fpwwe2lem11  10726  inar1  10860  grudomon  10902  axpre-sup  11254  un0addcl  12639  un0mulcl  12640  peano2uz2  12787  rpnnen1lem2  13105  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  xlemul1a  13418  fzadd2  13693  elfz2nn0  13752  fzind2  13923  expaddz  14249  expmulz  14251  swrdswrd  14854  cau3lem  15522  lo1bdd2  15691  climuni  15719  fsumcom2  15940  fprodcom2  16151  dvdsval2  16425  algcvga  16754  lcmgcdlem  16781  coprmproddvdslem  16837  divgcdcoprmex  16841  iserodd  17013  prmpwdvds  17082  ram0  17200  catpropd  17883  mndind  19024  isgrpinv  19204  gicsubgen  19493  sylow2alem2  19832  sylow2a  19833  frgpuptinv  19985  gsumcom3fi  20193  gsumxp2  20194  ablfac1eu  20289  dvdsrcl2  20596  isdrng4  20992  isdrng3lem2  21006  islss4  21237  ellspsn6  21269  lmhmima  21322  lsmcl  21358  prmidl0  21634  psgnodpm  21894  dsmmlss  22050  islindf4  22144  lindsenlbs  22157  gsumbagdiag  22240  psrass1lem  22241  coe1tmmul2  22595  dmatscmcl  22818  mdetdiaglem  22913  mdetunilem9  22935  matunitlindflem2  22995  pm2mp  23143  epttop  23327  neindisj  23435  neitr  23498  restcls  23499  restntr  23500  ordtrest2lem  23521  cncnp  23598  cnconst  23602  1stcrest  23771  2ndcdisj  23775  2ndcsep  23778  1stccnp  23781  islly2  23803  1stckgenlem  23872  ptbasin  23896  ptbasfi  23900  ptcnplem  23940  ptcnp  23941  tx1stc  23969  qtophmeo  24136  filconn  24202  filuni  24204  ufileu  24238  elfm3  24269  rnelfmlem  24271  fmfnfmlem4  24276  cnpflf2  24319  alexsubALTlem4  24369  ptcmplem3  24373  ptcmplem4  24374  ptcmplem5  24375  tsmsxplem1  24472  bl2in  24719  metcnpi  24863  metcnpi2  24864  metcnpi3  24865  recld2  25134  icoopnst  25260  iocopnst  25261  ncvs1  25478  iscfil3  25594  iscmet3lem2  25613  ovoliunlem1  25823  ovolicc2lem2  25839  ovolicc2lem4  25841  voliun  25875  volsuplem  25876  dyadmbllem  25920  mbfinf  25986  mbflimsup  25987  itg2seq  26063  itg2splitlem  26069  itg2cnlem1  26082  ellimc3  26199  dvnadd  26249  dvcnvlem  26296  c1liplem1  26316  lhop2  26335  coe1mul3  26417  ply1divex  26455  dvdsq1p  26481  preimaaa  26646  aannenlem1  26655  aalioulem2  26660  dvtaylp  26697  ulmdvlem3  26729  iblulm  26734  cxpmul2z  27019  xrlimcnp  27296  lgambdd  27364  wilthlem2  27396  basellem3  27410  dvdsflsumcom  27515  perfect  27558  dchreq  27585  dchrsum  27596  bposlem1  27611  lgsquad2  27713  dchrisum0fno1  27838  pntibnd  27920  nna4b4nsq  27990  noinfbnd1lem4  28083  cuteq1  28203  madebdaylemlrcut  28285  precsexlem11  28603  recsex  28605  bdayons  28662  addonbday  28665  noseqp1  28677  noseqrdgfn  28692  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  remulscllem2  28887  oppperpex  29229  lmieu  29289  ax5seglem5  29511  axeuclid  29541  egrsubgr  29858  nbumgrvtx  29927  wwlksnextsurj  30489  clwwlkccat  30581  numclwwlk2lem1lem  30943  nmcvcn  31297  ubthlem1  31472  leopmul2i  32737  hstel2  32821  atom1d  32955  cdj1i  33035  f1o3d  33220  fsuppcurry1  33316  fsuppcurry2  33317  xrge0addge  33350  mxidlmax  33990  reff  34471  ordtrest2NEWlem  34554  esumcst  34695  eulerpartlemgh  35010  cvmscld  36038  cgrxfr  36820  finminlem  37106  nn0prpwlem  37110  neibastop1  37147  neibastop2lem  37148  tailfb  37165  fvineqsneu  38335  pibt2  38341  finixpnum  38529  poimirlem4  38543  poimirlem25  38564  poimirlem26  38565  poimirlem29  38568  poimirlem30  38569  poimirlem31  38570  poimirlem32  38571  heicant  38574  mblfinlem3  38578  mblfinlem4  38579  itg2addnclem  38590  itg2addnclem3  38592  ftc1anc  38620  subspopn  38687  prdsbnd  38728  heibor1lem  38744  heiborlem1  38746  heibor  38756  isdrngo2  38893  rngoisocnv  38916  maxidlmax  38978  riotasv3d  40018  lkrpssN  40221  intnatN  40465  elpaddatiN  40863  pexmidlem5N  41032  lhpj1  41080  ltrnu  41179  cdlemn11pre  42268  dihord2pre  42283  dih1dimatlem0  42386  lcfrlem9  42608  remulcand  43491  prjspnnorm  43662  0prjspnrel  43664  rexrabdioph  43801  ctbnfien  43825  irrapxlem3  43831  elpell14qr2  43869  elpell1qr2  43879  kelac1  44065  iunrelexpuztr  44719  rfovcnvfvd  45007  radcnvrat  45298  nznngen  45300  tz6.12-afv  48243  tz6.12-afv2  48310  iccelpart  48515  prproropf1olem3  48587  lighneallem4  48695  perfectALTV  48821  bgoldbtbndlem3  48905  tgoldbach  48915  grimcnv  48986  grimco  48987  isuspgrim0  48992  grimedg  49033  isubgr3stgrlem7  49070  gpg5nbgrvtx03starlem1  49166  gpg5nbgrvtx03starlem3  49168  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem3  49171  isassintop  49307  ellcoellss  49547  lindslinindsimp2  49575  itscnhlinecirc02plem3  49896  inlinecirc02p  49899  aacllem  50939