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  3225  vtoclgft  3519  moi2  3677  preq12bg  4811  disjxiun  5103  disjxun  5104  wereu2  5652  frpomin  6358  f1ocnv2d  7695  funeldmdif  8081  extmptsuppeq  8230  suppssr  8237  suppssrg  8238  omeulem1  8615  oelim2  8629  oeoa  8631  boxriin  8993  frfi  9301  fipreima  9372  marypha1lem  9449  supiso  9492  ordtypelem10  9545  r1ordg  9809  infxpenc2lem1  10122  acndom  10154  acndom2  10157  cofsmo  10371  cfcoflem  10374  fin23lem28  10442  fin23lem36  10450  isf32lem1  10455  isf32lem2  10456  isf32lem5  10459  isf34lem4  10479  fin1a2lem6  10507  fin1a2s  10516  ttukeylem2  10612  ttukeylem6  10616  fpwwe2lem7  10746  fpwwe2lem11  10750  inar1  10884  grudomon  10926  axpre-sup  11278  un0addcl  12663  un0mulcl  12664  peano2uz2  12811  rpnnen1lem2  13129  rpnnen1lem1  13130  rpnnen1lem3  13131  rpnnen1lem5  13133  xlemul1a  13442  fzadd2  13717  elfz2nn0  13776  fzind2  13947  expaddz  14273  expmulz  14275  swrdswrd  14879  cau3lem  15548  lo1bdd2  15717  climuni  15745  fsumcom2  15966  fprodcom2  16177  dvdsval2  16451  algcvga  16780  lcmgcdlem  16807  coprmproddvdslem  16863  divgcdcoprmex  16867  iserodd  17039  prmpwdvds  17108  ram0  17226  catpropd  17909  mndind  19050  isgrpinv  19230  gicsubgen  19520  sylow2alem2  19859  sylow2a  19860  frgpuptinv  20012  gsumcom3fi  20220  gsumxp2  20221  ablfac1eu  20316  dvdsrcl2  20623  isdrng4  21019  isdrng3lem2  21033  islss4  21264  ellspsn6  21296  lmhmima  21349  lsmcl  21385  prmidl0  21661  psgnodpm  21921  dsmmlss  22077  islindf4  22171  lindsenlbs  22184  gsumbagdiag  22267  psrass1lem  22268  coe1tmmul2  22622  dmatscmcl  22845  mdetdiaglem  22940  mdetunilem9  22962  matunitlindflem2  23022  pm2mp  23170  epttop  23354  neindisj  23462  neitr  23525  restcls  23526  restntr  23527  ordtrest2lem  23548  cncnp  23625  cnconst  23629  1stcrest  23798  2ndcdisj  23802  2ndcsep  23805  1stccnp  23808  islly2  23830  1stckgenlem  23899  ptbasin  23923  ptbasfi  23927  ptcnplem  23967  ptcnp  23968  tx1stc  23996  qtophmeo  24163  filconn  24229  filuni  24231  ufileu  24265  elfm3  24296  rnelfmlem  24298  fmfnfmlem4  24303  cnpflf2  24346  alexsubALTlem4  24396  ptcmplem3  24400  ptcmplem4  24401  ptcmplem5  24402  tsmsxplem1  24499  bl2in  24746  metcnpi  24890  metcnpi2  24891  metcnpi3  24892  recld2  25161  icoopnst  25287  iocopnst  25288  ncvs1  25505  iscfil3  25621  iscmet3lem2  25640  ovoliunlem1  25850  ovolicc2lem2  25866  ovolicc2lem4  25868  voliun  25902  volsuplem  25903  dyadmbllem  25947  mbfinf  26013  mbflimsup  26014  itg2seq  26090  itg2splitlem  26096  itg2cnlem1  26109  ellimc3  26226  dvnadd  26276  dvcnvlem  26323  c1liplem1  26343  lhop2  26362  coe1mul3  26444  ply1divex  26482  dvdsq1p  26508  preimaaa  26673  aannenlem1  26682  aalioulem2  26687  dvtaylp  26724  ulmdvlem3  26756  iblulm  26761  cxpmul2z  27046  xrlimcnp  27323  lgambdd  27391  wilthlem2  27423  basellem3  27437  dvdsflsumcom  27542  perfect  27585  dchreq  27612  dchrsum  27623  bposlem1  27638  lgsquad2  27740  dchrisum0fno1  27865  pntibnd  27947  nna4b4nsq  28017  noinfbnd1lem4  28110  cuteq1  28230  madebdaylemlrcut  28312  precsexlem11  28630  recsex  28632  bdayons  28689  addonbday  28692  noseqp1  28704  noseqrdgfn  28719  bdaypw2n0bndlem  28876  bdayfinbndlem1  28880  remulscllem2  28914  oppperpex  29256  lmieu  29316  ax5seglem5  29538  axeuclid  29568  egrsubgr  29885  nbumgrvtx  29954  wwlksnextsurj  30516  clwwlkccat  30608  numclwwlk2lem1lem  30970  nmcvcn  31324  ubthlem1  31499  leopmul2i  32764  hstel2  32848  atom1d  32982  cdj1i  33062  f1o3d  33289  fsuppcurry1  33383  fsuppcurry2  33384  xrge0addge  33417  mxidlmax  34057  reff  34538  ordtrest2NEWlem  34621  esumcst  34762  eulerpartlemgh  35077  dfk12  36011  dfk22  36012  dfk32  36013  cvmscld  36204  cgrxfr  36997  finminlem  37283  nn0prpwlem  37287  neibastop1  37324  neibastop2lem  37325  tailfb  37342  fvineqsneu  38525  pibt2  38531  finixpnum  38719  poimirlem4  38733  poimirlem25  38754  poimirlem26  38755  poimirlem29  38758  poimirlem30  38759  poimirlem31  38760  poimirlem32  38761  heicant  38764  mblfinlem3  38768  mblfinlem4  38769  itg2addnclem  38780  itg2addnclem3  38782  ftc1anc  38810  subspopn  38877  prdsbnd  38918  heibor1lem  38934  heiborlem1  38936  heibor  38946  isdrngo2  39083  rngoisocnv  39106  maxidlmax  39168  riotasv3d  40208  lkrpssN  40411  intnatN  40655  elpaddatiN  41053  pexmidlem5N  41222  lhpj1  41270  ltrnu  41369  cdlemn11pre  42458  dihord2pre  42473  dih1dimatlem0  42576  lcfrlem9  42798  remulcand  43681  prjspnnorm  43852  0prjspnrel  43854  rexrabdioph  43992  ctbnfien  44016  irrapxlem3  44022  elpell14qr2  44060  elpell1qr2  44070  kelac1  44256  iunrelexpuztr  44909  rfovcnvfvd  45197  radcnvrat  45488  nznngen  45490  tz6.12-afv  48446  tz6.12-afv2  48513  iccelpart  48718  prproropf1olem3  48790  lighneallem4  48898  perfectALTV  49024  bgoldbtbndlem3  49108  tgoldbach  49118  grimcnv  49189  grimco  49190  isuspgrim0  49195  grimedg  49236  isubgr3stgrlem7  49273  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem3  49374  isassintop  49510  ellcoellss  49750  lindslinindsimp2  49778  itscnhlinecirc02plem3  50099  inlinecirc02p  50102  aacllem  51217