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  3223  vtoclgft  3518  moi2  3677  preq12bg  4816  disjxiun  5104  disjxun  5105  wereu2  5656  frpomin  6342  f1ocnv2d  7670  funeldmdif  8048  extmptsuppeq  8189  suppssr  8196  suppssrg  8197  omeulem1  8572  oelim2  8586  oeoa  8588  boxriin  8950  frfi  9258  fipreima  9328  marypha1lem  9406  supiso  9449  ordtypelem10  9502  r1ordg  9763  infxpenc2lem1  10025  acndom  10057  acndom2  10060  cofsmo  10274  cfcoflem  10277  fin23lem28  10345  fin23lem36  10353  isf32lem1  10358  isf32lem2  10359  isf32lem5  10362  isf34lem4  10382  fin1a2lem6  10410  fin1a2s  10419  ttukeylem2  10515  ttukeylem6  10519  fpwwe2lem7  10649  fpwwe2lem11  10653  inar1  10787  grudomon  10829  axpre-sup  11181  un0addcl  12564  un0mulcl  12565  peano2uz2  12712  rpnnen1lem2  13029  rpnnen1lem1  13030  rpnnen1lem3  13031  rpnnen1lem5  13033  xlemul1a  13342  fzadd2  13616  elfz2nn0  13675  fzind2  13846  expaddz  14172  expmulz  14174  swrdswrd  14776  cau3lem  15444  lo1bdd2  15613  climuni  15641  fsumcom2  15862  fprodcom2  16075  dvdsval2  16349  algcvga  16673  lcmgcdlem  16700  coprmproddvdslem  16756  divgcdcoprmex  16760  iserodd  16931  prmpwdvds  17000  ram0  17118  catpropd  17801  mndind  18938  isgrpinv  19118  gicsubgen  19407  sylow2alem2  19746  sylow2a  19747  frgpuptinv  19899  gsumcom3fi  20107  gsumxp2  20108  ablfac1eu  20203  dvdsrcl2  20508  isdrng4  20903  isdrng3lem2  20916  islss4  21147  ellspsn6  21179  lmhmima  21232  lsmcl  21268  prmidl0  21542  psgnodpm  21802  dsmmlss  21958  islindf4  22052  lindsenlbs  22065  gsumbagdiag  22148  psrass1lem  22149  coe1tmmul2  22503  dmatscmcl  22726  mdetdiaglem  22821  mdetunilem9  22843  matunitlindflem2  22903  pm2mp  23051  epttop  23235  neindisj  23343  neitr  23406  restcls  23407  restntr  23408  ordtrest2lem  23429  cncnp  23506  cnconst  23510  1stcrest  23679  2ndcdisj  23683  2ndcsep  23686  1stccnp  23689  islly2  23711  1stckgenlem  23780  ptbasin  23804  ptbasfi  23808  ptcnplem  23848  ptcnp  23849  tx1stc  23877  qtophmeo  24044  filconn  24110  filuni  24112  ufileu  24146  elfm3  24177  rnelfmlem  24179  fmfnfmlem4  24184  cnpflf2  24227  alexsubALTlem4  24277  ptcmplem3  24281  ptcmplem4  24282  ptcmplem5  24283  tsmsxplem1  24380  bl2in  24627  metcnpi  24771  metcnpi2  24772  metcnpi3  24773  recld2  25042  icoopnst  25168  iocopnst  25169  ncvs1  25386  iscfil3  25502  iscmet3lem2  25521  ovoliunlem1  25731  ovolicc2lem2  25747  ovolicc2lem4  25749  voliun  25783  volsuplem  25784  dyadmbllem  25828  mbfinf  25894  mbflimsup  25895  itg2seq  25971  itg2splitlem  25977  itg2cnlem1  25990  ellimc3  26108  dvnadd  26158  dvcnvlem  26205  c1liplem1  26225  lhop2  26244  coe1mul3  26326  ply1divex  26364  dvdsq1p  26390  aannenlem1  26561  aalioulem2  26566  dvtaylp  26603  ulmdvlem3  26635  iblulm  26640  cxpmul2z  26926  xrlimcnp  27203  lgambdd  27271  wilthlem2  27303  basellem3  27317  dvdsflsumcom  27422  perfect  27465  dchreq  27492  dchrsum  27503  bposlem1  27518  lgsquad2  27620  dchrisum0fno1  27745  pntibnd  27827  noinfbnd1lem4  27960  cuteq1  28080  madebdaylemlrcut  28162  precsexlem11  28480  recsex  28482  bdayons  28539  addonbday  28542  noseqp1  28554  noseqrdgfn  28569  bdaypw2n0bndlem  28726  bdayfinbndlem1  28730  remulscllem2  28764  oppperpex  29106  lmieu  29166  ax5seglem5  29376  axeuclid  29406  egrsubgr  29723  nbumgrvtx  29792  wwlksnextsurj  30354  clwwlkccat  30446  numclwwlk2lem1lem  30808  nmcvcn  31162  ubthlem1  31337  leopmul2i  32602  hstel2  32686  atom1d  32820  cdj1i  32900  f1o3d  33086  fsuppcurry1  33182  fsuppcurry2  33183  xrge0addge  33216  mxidlmax  33855  reff  34336  ordtrest2NEWlem  34419  esumcst  34560  eulerpartlemgh  34876  cvmscld  35839  cgrxfr  36622  finminlem  36924  nn0prpwlem  36928  neibastop1  36965  neibastop2lem  36966  tailfb  36983  fvineqsneu  38152  pibt2  38158  finixpnum  38346  poimirlem4  38360  poimirlem25  38381  poimirlem26  38382  poimirlem29  38385  poimirlem30  38386  poimirlem31  38387  poimirlem32  38388  heicant  38391  mblfinlem3  38395  mblfinlem4  38396  itg2addnclem  38407  itg2addnclem3  38409  ftc1anc  38437  subspopn  38489  prdsbnd  38530  heibor1lem  38546  heiborlem1  38548  heibor  38558  isdrngo2  38695  rngoisocnv  38718  maxidlmax  38780  riotasv3d  39820  lkrpssN  40023  intnatN  40267  elpaddatiN  40665  pexmidlem5N  40834  lhpj1  40882  ltrnu  40981  cdlemn11pre  42070  dihord2pre  42085  dih1dimatlem0  42188  lcfrlem9  42410  remulcand  43301  prjspner1  43459  0prjspnrel  43460  nna4b4nsq  43493  rexrabdioph  43622  ctbnfien  43646  irrapxlem3  43652  elpell14qr2  43690  elpell1qr2  43700  kelac1  43891  iunrelexpuztr  44546  rfovcnvfvd  44834  radcnvrat  45125  nznngen  45127  tz6.12-afv  48048  tz6.12-afv2  48115  iccelpart  48320  prproropf1olem3  48392  lighneallem4  48500  perfectALTV  48626  bgoldbtbndlem3  48710  tgoldbach  48720  grimcnv  48791  grimco  48792  isuspgrim0  48797  grimedg  48838  isubgr3stgrlem7  48875  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem3  48976  isassintop  49112  ellcoellss  49352  lindslinindsimp2  49380  itscnhlinecirc02plem3  49701  inlinecirc02p  49704  aacllem  50759