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  3193  vtoclgft  3507  moi2  3672  preq12bg  4807  disjxiun  5093  disjxun  5094  wereu2  5619  frpomin  6296  f1ocnv2d  7609  funeldmdif  7990  extmptsuppeq  8128  suppssr  8135  suppssrg  8136  omeulem1  8507  oelim2  8521  oeoa  8523  boxriin  8876  frfi  9183  fipreima  9256  marypha1lem  9334  supiso  9377  ordtypelem10  9430  r1ordg  9688  infxpenc2lem1  9927  acndom  9959  acndom2  9962  cofsmo  10177  cfcoflem  10180  fin23lem28  10248  fin23lem36  10256  isf32lem1  10261  isf32lem2  10262  isf32lem5  10265  isf34lem4  10285  fin1a2lem6  10313  fin1a2s  10322  ttukeylem2  10418  ttukeylem6  10422  fpwwe2lem7  10546  fpwwe2lem11  10550  inar1  10684  grudomon  10726  axpre-sup  11078  un0addcl  12432  un0mulcl  12433  peano2uz2  12578  rpnnen1lem2  12888  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem5  12892  xlemul1a  13201  fzadd2  13473  elfz2nn0  13532  fzind2  13702  expaddz  14027  expmulz  14029  swrdswrd  14626  cau3lem  15276  lo1bdd2  15445  climuni  15473  fsumcom2  15695  fprodcom2  15905  dvdsval2  16180  algcvga  16504  lcmgcdlem  16531  coprmproddvdslem  16587  divgcdcoprmex  16591  iserodd  16761  prmpwdvds  16830  ram0  16948  catpropd  17630  mndind  18751  isgrpinv  18921  gicsubgen  19206  sylow2alem2  19545  sylow2a  19546  frgpuptinv  19698  gsumcom3fi  19906  gsumxp2  19907  ablfac1eu  20002  dvdsrcl2  20300  islss4  20911  ellspsn6  20943  lmhmima  20997  lsmcl  21033  psgnodpm  21541  dsmmlss  21697  islindf4  21791  gsumbagdiag  21885  psrass1lem  21886  coe1tmmul2  22216  dmatscmcl  22445  mdetdiaglem  22540  mdetunilem9  22562  pm2mp  22767  epttop  22951  neindisj  23059  neitr  23122  restcls  23123  restntr  23124  ordtrest2lem  23145  cncnp  23222  cnconst  23226  1stcrest  23395  2ndcdisj  23398  2ndcsep  23401  1stccnp  23404  islly2  23426  1stckgenlem  23495  ptbasin  23519  ptbasfi  23523  ptcnplem  23563  ptcnp  23564  tx1stc  23592  qtophmeo  23759  filconn  23825  filuni  23827  ufileu  23861  elfm3  23892  rnelfmlem  23894  fmfnfmlem4  23899  cnpflf2  23942  alexsubALTlem4  23992  ptcmplem3  23996  ptcmplem4  23997  ptcmplem5  23998  tsmsxplem1  24095  bl2in  24342  metcnpi  24486  metcnpi2  24487  metcnpi3  24488  recld2  24757  icoopnst  24890  iocopnst  24891  ncvs1  25111  iscfil3  25227  iscmet3lem2  25246  ovoliunlem1  25457  ovolicc2lem2  25473  ovolicc2lem4  25475  voliun  25509  volsuplem  25510  dyadmbllem  25554  mbfinf  25620  mbflimsup  25621  itg2seq  25697  itg2splitlem  25703  itg2cnlem1  25716  ellimc3  25834  dvnadd  25885  dvcnvlem  25934  c1liplem1  25955  lhop2  25974  coe1mul3  26058  ply1divex  26096  dvdsq1p  26122  aannenlem1  26290  aalioulem2  26295  dvtaylp  26332  ulmdvlem3  26365  iblulm  26370  cxpmul2z  26654  xrlimcnp  26932  lgambdd  27001  wilthlem2  27033  basellem3  27047  dvdsflsumcom  27152  perfect  27196  dchreq  27223  dchrsum  27234  bposlem1  27249  lgsquad2  27351  dchrisum0fno1  27476  pntibnd  27558  noinfbnd1lem4  27692  cuteq1  27805  madebdaylemlrcut  27871  precsexlem11  28185  recsex  28187  bdayon  28240  noseqp1  28252  noseqrdgfn  28267  bdaypw2n0s  28420  remulscllem2  28446  oppperpex  28774  lmieu  28805  ax5seglem5  28955  axeuclid  28985  egrsubgr  29299  nbumgrvtx  29368  wwlksnextsurj  29922  clwwlkccat  30014  numclwwlk2lem1lem  30366  nmcvcn  30719  ubthlem1  30894  leopmul2i  32159  hstel2  32243  atom1d  32377  cdj1i  32457  f1o3d  32653  fsuppcurry1  32752  fsuppcurry2  32753  xrge0addge  32787  isdrng4  33326  prmidl0  33480  mxidlmax  33495  reff  33945  ordtrest2NEWlem  34028  esumcst  34169  eulerpartlemgh  34484  cvmscld  35416  cgrxfr  36198  finminlem  36461  nn0prpwlem  36465  neibastop1  36502  neibastop2lem  36503  tailfb  36520  fvineqsneu  37555  pibt2  37561  finixpnum  37745  lindsenlbs  37755  matunitlindflem2  37757  poimirlem4  37764  poimirlem25  37785  poimirlem26  37786  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  heicant  37795  mblfinlem3  37799  mblfinlem4  37800  itg2addnclem  37811  itg2addnclem3  37813  ftc1anc  37841  subspopn  37892  prdsbnd  37933  heibor1lem  37949  heiborlem1  37951  heibor  37961  isdrngo2  38098  rngoisocnv  38121  maxidlmax  38183  riotasv3d  39159  lkrpssN  39362  intnatN  39606  elpaddatiN  40004  pexmidlem5N  40173  lhpj1  40221  ltrnu  40320  cdlemn11pre  41409  dihord2pre  41424  dih1dimatlem0  41527  lcfrlem9  41749  remulcand  42636  prjspner1  42811  0prjspnrel  42812  nna4b4nsq  42845  rexrabdioph  42978  ctbnfien  43002  irrapxlem3  43008  elpell14qr2  43046  elpell1qr2  43056  kelac1  43247  iunrelexpuztr  43902  rfovcnvfvd  44190  radcnvrat  44497  nznngen  44499  tz6.12-afv  47361  tz6.12-afv2  47428  iccelpart  47621  prproropf1olem3  47693  lighneallem4  47798  perfectALTV  47911  bgoldbtbndlem3  47995  tgoldbach  48005  grimcnv  48076  grimco  48077  isuspgrim0  48082  grimedg  48123  isubgr3stgrlem7  48160  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem3  48261  isassintop  48398  ellcoellss  48623  lindslinindsimp2  48651  itscnhlinecirc02plem3  48972  inlinecirc02p  48975  aacllem  49988