Theorem impr 458

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  reximddv2  3223  vtoclgft  3522  moi2  3681  preq12bg  4813  disjxiun  5099  disjxun  5100  wereu2  5646  frpomin  6329  f1ocnv2d  7651  funeldmdif  8031  extmptsuppeq  8170  suppssr  8177  suppssrg  8178  omeulem1  8553  oelim2  8567  oeoa  8569  boxriin  8924  frfi  9231  fipreima  9303  marypha1lem  9381  supiso  9424  ordtypelem10  9477  r1ordg  9738  infxpenc2lem1  9977  acndom  10009  acndom2  10012  cofsmo  10228  cfcoflem  10231  fin23lem28  10299  fin23lem36  10307  isf32lem1  10312  isf32lem2  10313  isf32lem5  10316  isf34lem4  10336  fin1a2lem6  10364  fin1a2s  10373  ttukeylem2  10469  ttukeylem6  10473  fpwwe2lem7  10597  fpwwe2lem11  10601  inar1  10735  grudomon  10777  axpre-sup  11129  un0addcl  12516  un0mulcl  12517  peano2uz2  12663  rpnnen1lem2  12980  rpnnen1lem1  12981  rpnnen1lem3  12982  rpnnen1lem5  12984  xlemul1a  13293  fzadd2  13566  elfz2nn0  13625  fzind2  13796  expaddz  14121  expmulz  14123  swrdswrd  14720  cau3lem  15384  lo1bdd2  15553  climuni  15581  fsumcom2  15803  fprodcom2  16016  dvdsval2  16291  algcvga  16615  lcmgcdlem  16642  coprmproddvdslem  16698  divgcdcoprmex  16702  iserodd  16873  prmpwdvds  16942  ram0  17060  catpropd  17743  mndind  18864  isgrpinv  19037  gicsubgen  19321  sylow2alem2  19660  sylow2a  19661  frgpuptinv  19813  gsumcom3fi  20021  gsumxp2  20022  ablfac1eu  20117  dvdsrcl2  20417  islss4  21031  ellspsn6  21063  lmhmima  21116  lsmcl  21152  psgnodpm  21642  dsmmlss  21798  islindf4  21892  gsumbagdiag  21986  psrass1lem  21987  coe1tmmul2  22341  dmatscmcl  22565  mdetdiaglem  22660  mdetunilem9  22682  pm2mp  22887  epttop  23071  neindisj  23179  neitr  23242  restcls  23243  restntr  23244  ordtrest2lem  23265  cncnp  23342  cnconst  23346  1stcrest  23515  2ndcdisj  23518  2ndcsep  23521  1stccnp  23524  islly2  23546  1stckgenlem  23615  ptbasin  23639  ptbasfi  23643  ptcnplem  23683  ptcnp  23684  tx1stc  23712  qtophmeo  23879  filconn  23945  filuni  23947  ufileu  23981  elfm3  24012  rnelfmlem  24014  fmfnfmlem4  24019  cnpflf2  24062  alexsubALTlem4  24112  ptcmplem3  24116  ptcmplem4  24117  ptcmplem5  24118  tsmsxplem1  24215  bl2in  24462  metcnpi  24606  metcnpi2  24607  metcnpi3  24608  recld2  24877  icoopnst  25003  iocopnst  25004  ncvs1  25221  iscfil3  25337  iscmet3lem2  25356  ovoliunlem1  25566  ovolicc2lem2  25582  ovolicc2lem4  25584  voliun  25618  volsuplem  25619  dyadmbllem  25663  mbfinf  25729  mbflimsup  25730  itg2seq  25806  itg2splitlem  25812  itg2cnlem1  25825  ellimc3  25943  dvnadd  25993  dvcnvlem  26040  c1liplem1  26060  lhop2  26079  coe1mul3  26161  ply1divex  26199  dvdsq1p  26225  aannenlem1  26394  aalioulem2  26399  dvtaylp  26435  ulmdvlem3  26467  iblulm  26472  cxpmul2z  26758  xrlimcnp  27035  lgambdd  27103  wilthlem2  27135  basellem3  27149  dvdsflsumcom  27254  perfect  27297  dchreq  27324  dchrsum  27335  bposlem1  27350  lgsquad2  27452  dchrisum0fno1  27577  pntibnd  27659  noinfbnd1lem4  27792  cuteq1  27912  madebdaylemlrcut  27994  precsexlem11  28312  recsex  28314  bdayons  28371  addonbday  28374  noseqp1  28386  noseqrdgfn  28401  bdaypw2n0bndlem  28558  bdayfinbndlem1  28562  remulscllem2  28596  oppperpex  28928  lmieu  28959  ax5seglem5  29136  axeuclid  29166  egrsubgr  29480  nbumgrvtx  29549  wwlksnextsurj  30102  clwwlkccat  30194  numclwwlk2lem1lem  30546  nmcvcn  30900  ubthlem1  31075  leopmul2i  32340  hstel2  32424  atom1d  32558  cdj1i  32638  f1o3d  32830  fsuppcurry1  32928  fsuppcurry2  32929  xrge0addge  32962  isdrng4  33484  prmidl0  33639  mxidlmax  33655  reff  34138  ordtrest2NEWlem  34221  esumcst  34362  eulerpartlemgh  34677  cvmscld  35628  cgrxfr  36410  finminlem  36683  nn0prpwlem  36687  neibastop1  36724  neibastop2lem  36725  tailfb  36742  fvineqsneu  37910  pibt2  37916  finixpnum  38109  lindsenlbs  38119  matunitlindflem2  38121  poimirlem4  38128  poimirlem25  38149  poimirlem26  38150  poimirlem29  38153  poimirlem30  38154  poimirlem31  38155  poimirlem32  38156  heicant  38159  mblfinlem3  38163  mblfinlem4  38164  itg2addnclem  38175  itg2addnclem3  38177  ftc1anc  38205  subspopn  38256  prdsbnd  38297  heibor1lem  38313  heiborlem1  38315  heibor  38325  isdrngo2  38462  rngoisocnv  38485  maxidlmax  38547  riotasv3d  39589  lkrpssN  39792  intnatN  40036  elpaddatiN  40434  pexmidlem5N  40603  lhpj1  40651  ltrnu  40750  cdlemn11pre  41839  dihord2pre  41854  dih1dimatlem0  41957  lcfrlem9  42179  remulcand  43053  prjspner1  43213  0prjspnrel  43214  nna4b4nsq  43247  rexrabdioph  43376  ctbnfien  43400  irrapxlem3  43406  elpell14qr2  43444  elpell1qr2  43454  kelac1  43645  iunrelexpuztr  44300  rfovcnvfvd  44588  radcnvrat  44895  nznngen  44897  tz6.12-afv  47772  tz6.12-afv2  47839  iccelpart  48044  prproropf1olem3  48116  lighneallem4  48224  perfectALTV  48350  bgoldbtbndlem3  48434  tgoldbach  48444  grimcnv  48515  grimco  48516  isuspgrim0  48521  grimedg  48562  isubgr3stgrlem7  48599  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem3  48700  isassintop  48837  ellcoellss  49062  lindslinindsimp2  49090  itscnhlinecirc02plem3  49411  inlinecirc02p  49414  aacllem  50427