Theorem impr 459

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

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

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 401

This theorem is used by:  reximddv2  3223  vtoclgft  3519  moi2  3678  preq12bg  4817  disjxiun  5105  disjxun  5106  wereu2  5657  frpomin  6341  f1ocnv2d  7665  funeldmdif  8043  extmptsuppeq  8182  suppssr  8189  suppssrg  8190  omeulem1  8565  oelim2  8579  oeoa  8581  boxriin  8936  frfi  9243  fipreima  9313  marypha1lem  9391  supiso  9434  ordtypelem10  9487  r1ordg  9748  infxpenc2lem1  10010  acndom  10042  acndom2  10045  cofsmo  10259  cfcoflem  10262  fin23lem28  10330  fin23lem36  10338  isf32lem1  10343  isf32lem2  10344  isf32lem5  10347  isf34lem4  10367  fin1a2lem6  10395  fin1a2s  10404  ttukeylem2  10500  ttukeylem6  10504  fpwwe2lem7  10628  fpwwe2lem11  10632  inar1  10766  grudomon  10808  axpre-sup  11160  un0addcl  12543  un0mulcl  12544  peano2uz2  12690  rpnnen1lem2  13007  rpnnen1lem1  13008  rpnnen1lem3  13009  rpnnen1lem5  13011  xlemul1a  13320  fzadd2  13594  elfz2nn0  13653  fzind2  13824  expaddz  14149  expmulz  14151  swrdswrd  14749  cau3lem  15413  lo1bdd2  15582  climuni  15610  fsumcom2  15832  fprodcom2  16045  dvdsval2  16319  algcvga  16643  lcmgcdlem  16670  coprmproddvdslem  16726  divgcdcoprmex  16730  iserodd  16901  prmpwdvds  16970  ram0  17088  catpropd  17771  mndind  18893  isgrpinv  19066  gicsubgen  19355  sylow2alem2  19694  sylow2a  19695  frgpuptinv  19847  gsumcom3fi  20055  gsumxp2  20056  ablfac1eu  20151  dvdsrcl2  20455  isdrng4  20850  isdrng3lem2  20863  islss4  21094  ellspsn6  21126  lmhmima  21179  lsmcl  21215  prmidl0  21489  psgnodpm  21749  dsmmlss  21905  islindf4  21999  gsumbagdiag  22093  psrass1lem  22094  coe1tmmul2  22448  dmatscmcl  22671  mdetdiaglem  22766  mdetunilem9  22788  pm2mp  22993  epttop  23177  neindisj  23285  neitr  23348  restcls  23349  restntr  23350  ordtrest2lem  23371  cncnp  23448  cnconst  23452  1stcrest  23621  2ndcdisj  23624  2ndcsep  23627  1stccnp  23630  islly2  23652  1stckgenlem  23721  ptbasin  23745  ptbasfi  23749  ptcnplem  23789  ptcnp  23790  tx1stc  23818  qtophmeo  23985  filconn  24051  filuni  24053  ufileu  24087  elfm3  24118  rnelfmlem  24120  fmfnfmlem4  24125  cnpflf2  24168  alexsubALTlem4  24218  ptcmplem3  24222  ptcmplem4  24223  ptcmplem5  24224  tsmsxplem1  24321  bl2in  24568  metcnpi  24712  metcnpi2  24713  metcnpi3  24714  recld2  24983  icoopnst  25109  iocopnst  25110  ncvs1  25327  iscfil3  25443  iscmet3lem2  25462  ovoliunlem1  25672  ovolicc2lem2  25688  ovolicc2lem4  25690  voliun  25724  volsuplem  25725  dyadmbllem  25769  mbfinf  25835  mbflimsup  25836  itg2seq  25912  itg2splitlem  25918  itg2cnlem1  25931  ellimc3  26049  dvnadd  26099  dvcnvlem  26146  c1liplem1  26166  lhop2  26185  coe1mul3  26267  ply1divex  26305  dvdsq1p  26331  aannenlem1  26502  aalioulem2  26507  dvtaylp  26544  ulmdvlem3  26576  iblulm  26581  cxpmul2z  26867  xrlimcnp  27144  lgambdd  27212  wilthlem2  27244  basellem3  27258  dvdsflsumcom  27363  perfect  27406  dchreq  27433  dchrsum  27444  bposlem1  27459  lgsquad2  27561  dchrisum0fno1  27686  pntibnd  27768  noinfbnd1lem4  27901  cuteq1  28021  madebdaylemlrcut  28103  precsexlem11  28421  recsex  28423  bdayons  28480  addonbday  28483  noseqp1  28495  noseqrdgfn  28510  bdaypw2n0bndlem  28667  bdayfinbndlem1  28671  remulscllem2  28705  oppperpex  29045  lmieu  29104  ax5seglem5  29294  axeuclid  29324  egrsubgr  29638  nbumgrvtx  29707  wwlksnextsurj  30260  clwwlkccat  30352  numclwwlk2lem1lem  30704  nmcvcn  31058  ubthlem1  31233  leopmul2i  32498  hstel2  32582  atom1d  32716  cdj1i  32796  f1o3d  32982  fsuppcurry1  33080  fsuppcurry2  33081  xrge0addge  33114  mxidlmax  33757  reff  34238  ordtrest2NEWlem  34321  esumcst  34462  eulerpartlemgh  34777  cvmscld  35773  cgrxfr  36555  finminlem  36857  nn0prpwlem  36861  neibastop1  36898  neibastop2lem  36899  tailfb  36916  fvineqsneu  38085  pibt2  38091  finixpnum  38284  lindsenlbs  38294  matunitlindflem2  38296  poimirlem4  38303  poimirlem25  38324  poimirlem26  38325  poimirlem29  38328  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  heicant  38334  mblfinlem3  38338  mblfinlem4  38339  itg2addnclem  38350  itg2addnclem3  38352  ftc1anc  38380  subspopn  38431  prdsbnd  38472  heibor1lem  38488  heiborlem1  38490  heibor  38500  isdrngo2  38637  rngoisocnv  38660  maxidlmax  38722  riotasv3d  39762  lkrpssN  39965  intnatN  40209  elpaddatiN  40607  pexmidlem5N  40776  lhpj1  40824  ltrnu  40923  cdlemn11pre  42012  dihord2pre  42027  dih1dimatlem0  42130  lcfrlem9  42352  remulcand  43228  prjspner1  43386  0prjspnrel  43387  nna4b4nsq  43420  rexrabdioph  43549  ctbnfien  43573  irrapxlem3  43579  elpell14qr2  43617  elpell1qr2  43627  kelac1  43818  iunrelexpuztr  44473  rfovcnvfvd  44761  radcnvrat  45052  nznngen  45054  tz6.12-afv  47938  tz6.12-afv2  48005  iccelpart  48210  prproropf1olem3  48282  lighneallem4  48390  perfectALTV  48516  bgoldbtbndlem3  48600  tgoldbach  48610  grimcnv  48681  grimco  48682  isuspgrim0  48687  grimedg  48728  isubgr3stgrlem7  48765  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem3  48866  isassintop  49003  ellcoellss  49243  lindslinindsimp2  49271  itscnhlinecirc02plem3  49592  inlinecirc02p  49595  aacllem  50649