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  3197  vtoclgft  3498  moi2  3663  preq12bg  4797  disjxiun  5083  disjxun  5084  wereu2  5625  frpomin  6302  f1ocnv2d  7617  funeldmdif  7998  extmptsuppeq  8135  suppssr  8142  suppssrg  8143  omeulem1  8514  oelim2  8528  oeoa  8530  boxriin  8885  frfi  9192  fipreima  9265  marypha1lem  9343  supiso  9386  ordtypelem10  9439  r1ordg  9699  infxpenc2lem1  9938  acndom  9970  acndom2  9973  cofsmo  10188  cfcoflem  10191  fin23lem28  10259  fin23lem36  10267  isf32lem1  10272  isf32lem2  10273  isf32lem5  10276  isf34lem4  10296  fin1a2lem6  10324  fin1a2s  10333  ttukeylem2  10429  ttukeylem6  10433  fpwwe2lem7  10557  fpwwe2lem11  10561  inar1  10695  grudomon  10737  axpre-sup  11089  un0addcl  12467  un0mulcl  12468  peano2uz2  12614  rpnnen1lem2  12924  rpnnen1lem1  12925  rpnnen1lem3  12926  rpnnen1lem5  12928  xlemul1a  13237  fzadd2  13510  elfz2nn0  13569  fzind2  13740  expaddz  14065  expmulz  14067  swrdswrd  14664  cau3lem  15314  lo1bdd2  15483  climuni  15511  fsumcom2  15733  fprodcom2  15946  dvdsval2  16221  algcvga  16545  lcmgcdlem  16572  coprmproddvdslem  16628  divgcdcoprmex  16632  iserodd  16803  prmpwdvds  16872  ram0  16990  catpropd  17672  mndind  18793  isgrpinv  18966  gicsubgen  19251  sylow2alem2  19590  sylow2a  19591  frgpuptinv  19743  gsumcom3fi  19951  gsumxp2  19952  ablfac1eu  20047  dvdsrcl2  20343  islss4  20954  ellspsn6  20986  lmhmima  21039  lsmcl  21075  psgnodpm  21565  dsmmlss  21721  islindf4  21815  gsumbagdiag  21908  psrass1lem  21909  coe1tmmul2  22238  dmatscmcl  22465  mdetdiaglem  22560  mdetunilem9  22582  pm2mp  22787  epttop  22971  neindisj  23079  neitr  23142  restcls  23143  restntr  23144  ordtrest2lem  23165  cncnp  23242  cnconst  23246  1stcrest  23415  2ndcdisj  23418  2ndcsep  23421  1stccnp  23424  islly2  23446  1stckgenlem  23515  ptbasin  23539  ptbasfi  23543  ptcnplem  23583  ptcnp  23584  tx1stc  23612  qtophmeo  23779  filconn  23845  filuni  23847  ufileu  23881  elfm3  23912  rnelfmlem  23914  fmfnfmlem4  23919  cnpflf2  23962  alexsubALTlem4  24012  ptcmplem3  24016  ptcmplem4  24017  ptcmplem5  24018  tsmsxplem1  24115  bl2in  24362  metcnpi  24506  metcnpi2  24507  metcnpi3  24508  recld2  24777  icoopnst  24903  iocopnst  24904  ncvs1  25121  iscfil3  25237  iscmet3lem2  25256  ovoliunlem1  25466  ovolicc2lem2  25482  ovolicc2lem4  25484  voliun  25518  volsuplem  25519  dyadmbllem  25563  mbfinf  25629  mbflimsup  25630  itg2seq  25706  itg2splitlem  25712  itg2cnlem1  25725  ellimc3  25843  dvnadd  25893  dvcnvlem  25940  c1liplem1  25960  lhop2  25979  coe1mul3  26061  ply1divex  26099  dvdsq1p  26125  aannenlem1  26291  aalioulem2  26296  dvtaylp  26332  ulmdvlem3  26364  iblulm  26369  cxpmul2z  26652  xrlimcnp  26929  lgambdd  26997  wilthlem2  27029  basellem3  27043  dvdsflsumcom  27148  perfect  27191  dchreq  27218  dchrsum  27229  bposlem1  27244  lgsquad2  27346  dchrisum0fno1  27471  pntibnd  27553  noinfbnd1lem4  27687  cuteq1  27806  madebdaylemlrcut  27888  precsexlem11  28206  recsex  28208  bdayons  28265  addonbday  28268  noseqp1  28280  noseqrdgfn  28295  bdaypw2n0bndlem  28452  bdayfinbndlem1  28456  remulscllem2  28490  oppperpex  28818  lmieu  28849  ax5seglem5  28999  axeuclid  29029  egrsubgr  29343  nbumgrvtx  29412  wwlksnextsurj  29965  clwwlkccat  30057  numclwwlk2lem1lem  30409  nmcvcn  30763  ubthlem1  30938  leopmul2i  32203  hstel2  32287  atom1d  32421  cdj1i  32501  f1o3d  32696  fsuppcurry1  32794  fsuppcurry2  32795  xrge0addge  32828  isdrng4  33353  prmidl0  33507  mxidlmax  33522  reff  33980  ordtrest2NEWlem  34063  esumcst  34204  eulerpartlemgh  34519  cvmscld  35452  cgrxfr  36234  finminlem  36497  nn0prpwlem  36501  neibastop1  36538  neibastop2lem  36539  tailfb  36556  fvineqsneu  37724  pibt2  37730  finixpnum  37923  lindsenlbs  37933  matunitlindflem2  37935  poimirlem4  37942  poimirlem25  37963  poimirlem26  37964  poimirlem29  37967  poimirlem30  37968  poimirlem31  37969  poimirlem32  37970  heicant  37973  mblfinlem3  37977  mblfinlem4  37978  itg2addnclem  37989  itg2addnclem3  37991  ftc1anc  38019  subspopn  38070  prdsbnd  38111  heibor1lem  38127  heiborlem1  38129  heibor  38139  isdrngo2  38276  rngoisocnv  38299  maxidlmax  38361  riotasv3d  39403  lkrpssN  39606  intnatN  39850  elpaddatiN  40248  pexmidlem5N  40417  lhpj1  40465  ltrnu  40564  cdlemn11pre  41653  dihord2pre  41668  dih1dimatlem0  41771  lcfrlem9  41993  remulcand  42868  prjspner1  43056  0prjspnrel  43057  nna4b4nsq  43090  rexrabdioph  43219  ctbnfien  43243  irrapxlem3  43249  elpell14qr2  43287  elpell1qr2  43297  kelac1  43488  iunrelexpuztr  44143  rfovcnvfvd  44431  radcnvrat  44738  nznngen  44740  tz6.12-afv  47612  tz6.12-afv2  47679  iccelpart  47884  prproropf1olem3  47956  lighneallem4  48064  perfectALTV  48190  bgoldbtbndlem3  48274  tgoldbach  48284  grimcnv  48355  grimco  48356  isuspgrim0  48361  grimedg  48402  isubgr3stgrlem7  48439  gpg5nbgrvtx03starlem1  48535  gpg5nbgrvtx03starlem3  48537  gpg5nbgrvtx13starlem1  48538  gpg5nbgrvtx13starlem3  48540  isassintop  48677  ellcoellss  48902  lindslinindsimp2  48930  itscnhlinecirc02plem3  49251  inlinecirc02p  49254  aacllem  50267